Title: Controllability for discrete event systems modelled in VeriJ

 

Author: Yan Zhang; Béatrice Bérard; Lom Messan Hillah; Fabrice Kordon; Yann Thierry-Mieg

 

Addresses:
Université Pierre and Marie Curie, CNRS-UMR 7606 (LIP6/MoVe), 4 Place Jussieu, F-75005 Paris, France
Université Pierre and Marie Curie, CNRS-UMR 7606 (LIP6/MoVe), 4 Place Jussieu, F-75005 Paris, France
Université Pierre and Marie Curie, CNRS-UMR 7606 (LIP6/MoVe), 4 Place Jussieu, F-75005 Paris, France; Université Paris Ouest Nanterre La Défense, 200, Avenue de la République, F-92001 Nanterre Cedex, France
Université Pierre and Marie Curie, CNRS-UMR 7606 (LIP6/MoVe), 4 Place Jussieu, F-75005 Paris, France
Université Pierre and Marie Curie, CNRS-UMR 7606 (LIP6/MoVe), 4 Place Jussieu, F-75005 Paris, France

 

Journal: Int. J. of Critical Computer-Based Systems, 2014 Vol.5, No.3/4, pp.218 - 240

 

Abstract: Existing tools for controllability checking mostly apply to abstract formalisms like finite automata or Petri nets. To avoid costly building of low-level formal models for large complex systems, we propose a programming language called VeriJ, a subset of Java with additional constructs dedicated to supervisory control, to model these systems in a familiar and friendly development environment. We provide a prototype tool chain, based on model transformation and pushdown automata, to automatically transform a system described in VeriJ into a labelled transition system (LTS). A controllability engine for this LTS is then integrated to the tool. To limit the state space explosion problem, we also add several mechanisms including garbage collection, abstraction, state compression, and partial exploration. Our approach, illustrated with a VeriJ model of the Nim game, shows that it is possible to combine: 1) the benefits resulting from using mature Java development environments; 2) performances comparable to those of existing tools.

 

Keywords: VeriJ; Java; model transformation; verification; controllability checking; discrete event systems; critical systems; systems modelling; supervisory control; pushdown automata; labelled transition system; LTS.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2014.064668

 

Available online 03 Sep 2014

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article