VeriJ   A language for modeling complex discrete event systems



What is VeriJ
Publications
Download
Contact us

What is VeriJ

VeriJ is a language designed for modeling complex supervisory control problems. VeriJ is based on a subset of the Java language with some supervisory control specific constructs added; this allows to use industrial strength integrated development environments such as Eclipse to build VeriJ models and to
directly use a Java debugger to execute (simulate) these models. With the aim to perform controller synthesis in a further step, VeriJ models are translated into hierarchical finite state machines (HFSM) representing the control flow graph, using modern model transformation techniques and tools. The semantics of these HFSM is then given as a pushdown system, leading to a concise and expressive representation of the underlying discrete event system. We illustrate our modeling and transformation approach with a VeriJ model of the Nim game, for which finding a winning strategy for a player can be seen as a control problem.
VeriJ consists of a subset of the Java language, including elements such as: basic data types, arithmetic operators, assignments, decision and control statements, construction of classes with instantiation, with the addition of specific classes described below. VeriJ does not support features such as cast, exceptions, visibility, inheritance, libraries or native code (see Figure 1).


Figure 1. Illustration of VeriJ definition

To apply formal analysis to VeriJ models, VeriJ source code is compiled into a Hierarchical Finite State machine (HFSM), i.e. a set of finite state machines. The transformation (Figure 2) includes preprocessing and compilation, using model transformation techniques involving metamodels. Since VeriJ takes a subset of Java, its metamodel is primarily derived from the metamodel of Java, by removing 46 metaclasses (from the 126 metaclasses of Java) and adding the new elements. Despite the classes removed from Java metamodel, VeriJ metamodel is still too large to be displayed in this paper. To get an in-depth description and complete details of the Java metamodel, we refer the reader to http://wiki.eclipse.org/MoDisco/Component/Java/Documentation/0.9.

In the preprocessing step, we extract the Java model of the application, conforming to Java metamodel, from either the Java source code or the VeriJ source code, thanks to MoDisco. MoDisco is a model-driven framework providing tools to support software modernization. Among these tools, discoverers automatically create models of existing systems. The VeriJ model, conforming to VeriJ metamodel, built out of the extracted Java model, is obtained by pruning unnecessary information from the Java model and building the VeriJ specific elements. Given the Java metamodel and the VeriJ metamodel, this step is carried out by a set of rules Java2VeriJ.atl, using Atlas Transformation Language (ATL) framework.

m2m
Figure 2. From source code to formal model

The control flow of a VeriJ model can be syntactically described by a Hierarchical Finite State Machine (HFSM), which is a finite set of finite automata, linked together according to program instructions. The core part of HFSM is shown in Figure 3.  Using VeriJ metamodel and HFSM metamodel, we code a set of ATL rules VeriJ2Hfsm.atl to create the states and transitions for each FSM in this HFSM model. To visualize the obtained HFSM model described in the form of XML Metadata Interchange, we create the corresponding .dot file through project FSM2Dot and then generate the hierarchical FSM diagrams using Graphviz.

Figure 3. Core part of HFSM metamodel

It is well known that FSMs are not expressive enough to describe program semantics. For example, method calls and returns need to be correctly matched, including recursion schemes. Local variables in different procedure calls need to be distinguished. Pushdown systems (PDS), introduced in 1961 are a natural choice for modeling method calls and interprocedural program behaviours, by adding a (possibly unbounded) stack to a finite set of control states. Pushdown systems are used in several recent verification tools (e.g. jMoped for Java and MOPS or Magic for C) to describe programs when recursion is involved. In fact, pushdown systems give a formal semantics to programs.

Here are the toy examples about the modeling and transformations.

Controller Synthesis

Controller synthesis for discrete event systems, introduced in the seminal work of Ramadge and Wonham, answers the following question: given a model M and a specification expressed as a formula fi, does there exist a controller C such that the composition of C and M satisfies the specification? Typically, the property fi is a predicate on system states describing avoidance of undesirable situations (deadlocks, buffer overflow, etc.).
The problem can be viewed as a two-player game, environment versus controller, where the environment tries to bring the system into a failure state. The problem is then to find a winning strategy for the controller, if it exists. To solve this problem, in a transition system over a set of actions Act, the classical algorithm consists in a backward exploration of the set Sreach of reachable states: starting from Sfail, the set of currently (bad) reachable states that must be avoided, (1) any state from which the environment can reach a failure state in a single move is added to Sfail and (2) any state from which all controller moves lead to a failure state is added to Sfail. When a fixpoint is reached, either the initial state is a failure state, indicating that the system is not controllable, or there exists a winning strategy for the controller. In the latter case, controller synthesis consists in the construction of such a winning strategy. A (memoryless) strategy is a function f : Sc-->2Act which maps each state where the controller can act to an appropriate set of actions. Based on the set Sfail computed by the algorithm, a winning strategy ensures that the system stays in the set Ssafe = Sreach \ Sfail of safe states.
If the initial state is in the set Ssafe, the system is controllable. If this first controllability check is unsuccessful, the user should iteratively update the model to either restrict the environment, enlarge the potential actions of the controller, or increase the information sent to the controller.

Users can define a controller as a specially designated VeriJ class implementing the VeriJ.choice method, that will be called at any decision point and return the index of the selected action. The user should assign to attributes of the controller references to relevant parts of the system, typically some kind of entry point from which the controller context can navigate to explore all model elements.

This process is iterative as shown in Fig. 4, and should be started from a controllable system. It consists in first writing a skeleton for the controller, by discarding obviously (to the designer) bad choices and calling the VeriJ choice method (again) with a more limited set of actions if the decision to take is not obvious. At each step of the process, the user can confirm his intuition by running the tool and checking that the system (under the restriction of player actions that his controller represents) is still controllable. When the controller is not yet fully deterministic, the tool can synthesize deterministic code to insert at these choice points, as explained above. Ultimately the user can build a fully deterministic controller with no calls to the VeriJ choice method; if the system is still controllable, it means he has designed a winning strategy. As the controller is refined during this process, the set of possible system executions will be reduced (since it is more deterministic), allowing the tool to scale to larger parameter values.


Fig. 4  Iterative refinement of user-defined controller.

Publications

[1] Modeling Automated Highway Systems with VeriJ. In MOdelling and VErifying parallel Processes (MOVEP), pages 138–143. [pdf]
     ---- In this paper, we proposed the idea and definition of VeriJ and its application on a complex system.

[2] Modeling complex systems with VeriJ. Y. Zhang, B. Bérard, L.M. Hillah, F. Kordon, Y. Thierry‑Mieg, 5th International Workshop on Verification and Evaluation of Computer and Communication Systems  (VECoS'11), Tunis, Tunisia. [pdf]
    ---- In this paper, we explained how to use VeriJ and gave the transformation from Java program to VeriJ model and then to formal models.

[3] Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams, Y. Zhang, B. Bérard, F. Kordon, Y. Thierry‑Mieg, 11th International Workshop on Discrete Event Systems (WODES'10), Berlin,      Germany, pp. 291-296, (IFAC/Elsevier). [pdf]
    ---- In this paper, we explained how to tackle the controllability and verification for a complex system. We will link this work with the PDS model generated together.

Download

If you want to access the work around VeriJ, welcome to browse the svn and have a look at the source code first please:
https://srcdev.lip6.fr/trac/research/yzhang/browser
The download version will be available soon.

Contact

Yan.Zhang@lip6.fr