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 indepth 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 modeldriven 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.
Figure 2. From source code to formal model

Hierarchical Finite State
Machine (HFSM)
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 twoplayer 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.

Automatically generated 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 userdefined 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, 5^{th}
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, 11^{th} International Workshop on
Discrete Event Systems (WODES'10), Berlin,
Germany, pp. 291296, (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