(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.


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.


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


Tool list

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


          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
         The file format of Fc2tools is  called .fc2.



The following is a set of tools we built to facilitate compositional analysis.   They can be downloaded here: ArCats\
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)


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.

=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.

to be continued




Design framework