Controllability for discrete event systems modelled in VeriJ
by Yan Zhang; Béatrice Bérard; Lom Messan Hillah; Fabrice Kordon; Yann Thierry-Mieg
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 5, No. 3/4, 2014

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.

Online publication date: Tue, 21-Oct-2014

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com