ArCats 

(Architecture Refactoring and Compositional Analysis Tool Suite)

Author: Yung-Pin Cheng

Welcome to the homepage of ArCats.  ArCats stands for Architecture Refactoring and Compositional Analysis Tool Suite. Our research goal is to build a set of prototype tools to facilitate compositional analysis.

Compositional analysis avoids state explosion by dividing a whole system into many subsystems. Ideally, the analysis of each subsystem would produce manageable and smaller state space and then each subsystem can be replaced by a simple interface process. The process is continued by combining the analysis of subsystems into a larger subsystems in a hierarchical fashion until the whole system is analyzed. Unfortunately, this ideal scenario seldom happens in practical cases. Compositional analysis is architecture sensitive. In many systems, no feasible hierarchies exist in their as-built architecture;  that is, The power of divide-and-conquer is often limited by the system architecture.

Refactoring: The refactoring consists a set of transformations. Each transformation maintains the behavioral equivalence (weak bisimulation) of the model. By applying a sequence of transformations, a model P is gradually transformed into a model P' with new structure which is more amenable to compositional analysis. It consists in building a sequence of equivalent models, each obtained by the preceding ones by means of the application of a rule. The rules are aimed for restructuring the as-built structures
which are not suitable for compositional techniques. The goal is to obtain a transformed model whose structure contains loosely coupled components, where processes in each component do not yield state explosion.

Publications

n      Yung-Pin Cheng  “Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices",  Technical Report, National Taiwan Normal University. PDF  

n      Yung-Pin Cheng, Michal Young, Che-Ling Huang, and Chia-Yi Pan, “Towards Scalable Compositional Analysis by Refactoring Design Models", Proceedings of the ACM SIGSOFT 2003 Symposium on the Foundations of Software Engineering (FSE2003) , Helsinki, Finland, Sep. 2003. (also appear in      ACM Software Engineering Notes, pp. 247-256, Vol 28 ,Issue 5, 2003.)   PDF   PS

n      Yung-Pin Cheng, “Refactoring Design Models for Inductive Verification,” Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis. (ISSTA2002) Rome, Italy, July 22-24, 2002. (also appear in ACM Software Engineering Notes , pp 164-168, Vol. 27, No. 4 2002.)  PDF  PS

n        Yung-Pin Cheng and Keh-Ren Wu “Reasoning about Many Data Values without Data Independence Constraints”, In Proceedings of 1st International Workshop on Automated Technology for Verification and Analysis, 2003, Taipei, Taiwan.

News & Words from the Authors

2005/3/31 Most of the tools released in this homepage is completed or rewritten by myself.  There were some tools coded by my graduates (Master students). However, those tools were not stable and have lots of bugs. So, the tools listed in this homepage are mostly completed  or rewritten by myself.  This year, two of my graduates are working on tools to replace Fc2tools. So far, their results seem to be successful. Some of the tools, however, is under my implementation. However, with the teaching load and family life, the progress can be slow sometimes.  We will try our best to release tools under developing when they are stable.

Environment

To obtain best portability, our project is coded under standard GNU C++ . The environment is CYGWIN. It should be no problem to be ported to Linux environment. However, in current stage, we borrow some tools from other research institution. Some of them can only be executed under Linux.

Windows - CYGWIN

LINUX

Tool list

The following is a list of  tools. Click on the name will bring you to download it.

---------------------------------------------------------------

• Fc2tools -  These tools were developed from INRIA, France. It includes a set of tools to compose and minimize state graph in CCS semantics (paired communication).  Currently Fc2tools are used as our state enumeration engine.  These tools will be replaced in the near future.

          Their tools include
                    fc2explicit:   to explore reachable states without using OBDD
                    fc2implicit:   to explore reachable states using OBDD
                    fc2min:         compute strong, branch, and weak bisimulation of a state graph
                    fc2link:         check label consistency among .fc2 files before state enumeration.        
                    atg:               a graphical program to input state graphs of processes and save them as .fc2

         They can be download at http://www-sop.inria.fr/meije/verification/doc.html
         The file format of Fc2tools is  called .fc2.

---------------------------------------------------------------

• Dot - Graph visualization is a way of representing structural information as diagrams of abstract graphs and networks. Automatic graph drawing has many important applications in software engineering, database and web design, networking, and in visual interfaces for many other domains. It can be downloaded at http://www.graphviz.org/
  
  Dot has been widely used as a graph visualization tool. We use its file format .dot to describe the state graphs of processes. When we want to verify a system, we translate these state graphs into .fc2 format to be read by Fc2tools.

---------------------------------------------------------------

The following is a set of tools we built to facilitate compositional analysis.   They can be downloaded here: ArCats\dotfc2tool.zip.
Some of these tools currently rely on Fc2tools. Some are not. Our future plan is to replace Fc2tools. Then, all of the tools
listed here can be executed under Linux or Windows (CYGWIN)

• promela-front (with ADT) - 
                        usage: promela-front  .la
                        download:  ArCats\adt-promela.exe (cygwin version)
                        This tool reads a promela file and produce several files. For example, suppose an example file ex1.la
                              contains two processes p and q. if you use promela-front ex1.la
                        it will generate the following files
                                   ex1_sym.tab     - the symbol table which is shared by the process in ex1.la
                                   ex1_p.cfg         - the control flow state graph of process p
                                   ex1_p.cfg.dot   -  the dot file of control flow state graph of process P. It can be read by DOT.
                                   ex1_q.cfg         - the control flow state graph of process q
                                   ex1_q.cfg.dot   - the dot file of control flow state graph of process q. It can be read by DOT.
                             This promela front-end can process most of Promela syntax. Two abstract data types are added to
                             this prototype tool. They are set and queue. 
  　
• composefc2 -  
                             usage:  composefc2  name  .fc2 .fc2 ......
                             This tool compose a set of .fc2 files into a subsystem. name is the new name of the subsystem. The shell script
                             automatically treat other .fc2 files in the directory as environment. For example, suppose a directory has p.fc2 q.fc2   
                             and r.fc2. When you invoke
                                   composefc2 pq p.fc2 q.fc2
                             The composefc2 will automatically treat r.fc2 as the environment and then determine which labels in pq.fc2
                             should be exported. (i.e., not to be restricted)
  
                           
• chkconsist-    
                      usage:   chkconsist .dot .dot ......
                      This tool a set of state graphs described in .dot to see if there are any errors or unmatched
                           rendervous labels exist in these state graph.  This tool is very useful, especially if your state graphs are input
                           using atg of Fc2tools. It will check if there are rendezvous labels which do not have matched labels in
                           other state graphs. Fc2tools do not check that. Use this tool before compose any system. This tool make sure
                           you compose a correct system.
                      
                      
• chkconsistfc2 -
                     usage: chkconsist .fc2 .fc2 .....
                         Same as chkconsist. The difference is that the file are of .fc2 format
  　
• gendotstruct -
                     usage: gendotstruct systemname .dot .dot .dot
                          This tool collects a set of .dot files. These files are supposed to be composed into a system called systemname.
                          This tool reads all the state graphs and compute their interactions among each other and then draw their interaction
                          into a dot file. Later, we can use dot2ps to translate it into a postscript file to show the synchronization structure
                           among processes. This tool is very useful for finding a feasible composing hierarchy.  An example
                          synchronization structure is ArCats\chiron.struct.ps.  A rendezvous between two processes is represented by one
                          line. So, processes that are tightly-coupled may have several lines between them because they communicate by many
                          rendezvous.
• =to be continued
  　
• genfc2struct 
• composehi
• dot2fc2
• fc2dot
• dotpurge
• dot2ps
• dot2gif
• 
  　

Examples

The following is the models of examples which have been described in our published paper.

=Elevator system

The model of elevator system is extracted from the elevator system of Richardson et al. \cite{RAO:oracles-icse}. Its implementation uses array of Ada tasks and is designed to be extended to arbitrary number of elevators. If the number of elevators is $n$, there are $n+3$ tasks, including $n$ $elev\_sim\_task[i]$ which emulate the moving elevators for lifting customers, one \emph{controller} task to command elevators to serve hall calls or car calls, one command dispatcher task (\emph{elevator}), and one task (\emph{driver}) to emulate customer pushing the hall call or car call button.

• Models that described in .dot  files
  two elevators version:   ArCats\models\elev_2.zip
  three elevators version: ArCats\models\elev_3.zip
  four elevator version:    ArCats\models\elev_4.rar
  five elevator version:    ArCats\models\elev_5.rar
  　
• Models that descrined in an Ada-like language called Pal
  ArCats\models\elev_ada_pal.rar
  　
• Refactored models in .dot file format
  one elevator version:  ArCats\models\elev_1_refactored.rar
  　

=Chiron User Interface system

The first example is called Chiron user interface \cite{Keller:Chiron-1-ICSE13}.It has been analyzed by \cite{Avrunin:Chiron,Young:CATS}. Chiron user interface system is originally written in Ada. Chiron's design philosophy is to separate application code from user interface code.
So, there are user interface agents called \emph{artists} attached to selected data% \footnote{You can consider the data as an object and the object's values (or attributes) is linked to a visualization tool called artists. In other words, an artist can be viewed as a graphic drawing unit for the data.% } belonging to the applications. At runtime, each artist can register \emph{events} of interests to \emph{dispatcher.} Whenever there is
an operation call on the data, the dispatcher intercepts the call  and notifies each of the artists associated with that data with the event.

• Models that described in Ada-like language
  ArCats\models\chiron.ada
  　
• Models that described in native Promela
  ArCats\models\chiron.la
  　
• dispatcher_task  that described in ADT-Promela (for testing purpose only)
  ArCats\models\dispatcher_ADT.la
  
  　
• Refactored models that described in .dot format
  2 artist 2 event version:    ArCats\models\a2e2.rar ,
            synchronization structure ArCats\models\chiron.struct.ps  generated by gendotstruct
  
  3 artist 2 event version:  ArCats\models\a3e2.rar
  5 artist 2 event version:  ArCats\models\a5e2.rar
  10 artist 2 event version:ArCats\models\a10e2.rar
  　

to be continued

Design framework