 |
ADL2N is a multiplatform tool written in Java that provides an easy generation of behaviour models for the Fractal Component Model. Starting from a component specification written in ADL (Architecture Description Language), this application automatically generates the behaviour model expressed as an Labelled Transition System (in FC2 format). As input, the user should provide the ADL and implementations of the interfaces defined within the ADL (needed to extract methods signatures), and the behaviour of each primitive component (in the current version it is not yet mandatory) in either FC2 or LOTOS code.
Although the output model is parameterized, there are no model-checking available that can handle them. Fortunately, they can easily instantiated and then used in finite-state model-checking tools. Once created, the model can be directly used with CADP to check several properties such as deadlock freedom, liveness, fairness or reachability. In future versions the user may check non-functional properties, thus reconfiguration problems may be found before actually launching the application.
This application fits within the Vercors framework currently developed at the OASIS Project from INRIA Sophia-Antipolis. We are building a tool platform (see figure 1) for the analysis and verification of safety and security properties of distributed applications. The central component of the platform is a method for generating finite models for distributed applications, from static analysis of source code. We base this generation procedure on the strong semantic features provided by the ProActive library, and we generate compositional models using synchronised labelled transition systems. Various tools for static analysis, model checking, and equivalence checking can then operate on these models. One long term goal of this work is to integrate the various techniques and tools involved in this software platform, so that the platform can be integrated in a development environment, and used by non-specialists. At the same time, the platform must be flexible and open enough to serve as a basis for easy prototyping of new techniques and tools on real Java/ProActive code.
The FC2 format [2,8] was originally designed to interface several preexisting verification tools [7]. In this way these heterogeneous tools could be further developed independently, while being used in cooperation with their complementary features.
The format allows description of labelled transition systems and networks of communicating automata. While the format is not "syntax-friendly" (as it represent objects which are supposedly obtained by translation or compilation), it is still reasonably natural: automata are tables of states, states being each in turn a table of outgoing transitions with target indexes; networks are vectors of references to subcomponents (i.e., to other tables), together with synchronisation vectors (legible combinations of subcomponent behaviours acting in synchronised fashion). Subcomponents can be networks themselves, allowing hierarchical descriptions.
LOTOS (Language of Temporal Ordering Specification) is one of the two Formal Description Techniques (FDT) [6,5] developed within ISO (International Standards Organisation) for the formal specification of open distributed systems, and in particular for those related to the Open Systems Interconnection (OSI) computer network architecture [4]. The basic idea that LOTOS developed from was that systems can be specified by defining the temporal relation among the interactions that constitute the externally observable behaviour of a system. Contrary to what the name seems to suggest, this description technique is not related to temporal logic, but is based on process algebraic methods. More specifically, the component of LOTOS that deals with the description of process behaviours and interactions has borrowed many ideas from [9,3].