Skip to main content
No Access

Controllability for discrete event systems modelled in VeriJ

Published Online:pp 218-240https://doi.org/10.1504/IJCCBS.2014.064668

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, discrete event systems, critical systems

References

  • 1. Bérard, B. , Haddad, S. , Hillah, L. , Kordon, F. , Thierry-Mieg, Y. (2008). ‘Collision avoidance in intelligent transport systems: towards an application of control theory’. in Proc. of the 9th Int. Workshop on Discrete Event Systems (WODES ‘08). IEEE Press, 346-351 Google Scholar
  • 2. Ball, T. , Levin, V. , Rajamani, S. (2011). ‘A decade of software model checking with SLAM’. Communications of the ACM. 54, 7, 68-76 Google Scholar
  • 3. Behrmann, G. , Cougnard, A. , David, A. , Fleury, E. , Larsen, K. , Lime, D. (2007). ‘UPPAAL-TIGA: time for playing games!’. in Proc. of the 19th International Conference on Computer Aided Verification (CAV ‘07), Lecture Notes in Computer Science. 4590, Springer, 121-125 Google Scholar
  • 4. Beyer, D. , Henzinger, T.A. , Jhala, R. , Majumdar, R. (2007). ‘The software model checker blast’. International Journal on Software Tools for Technology Transfer (STTT). 9, 5, 505-525 Google Scholar
  • 5. Bogdoll, J. , Fioriti, L.F. , Hartmanns, A. , Hermanns, H. (2011). ‘Partial order methods for statistical model checking and simulation’. in Proc. of Joint 13th IFIP WG 6.1 International Conference on Formal Methods for Open Object-based Distributed Systems and 31st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FMOODS/FORTE), Lecture Notes in Computer Science. 6722, Springer, 59-74 Google Scholar
  • 6. Bogholm, T. , Kragh-Hansen, H. , Olsen, P. , Thomsen, B. , Larsen, K. (2008). ‘Model-based schedulability analysis of safety critical hard real-time Java programs’. in Proc. of the 6th Int. Workshop on Java Technologies for Real-time and Embedded Systems. ACM Press, 106-114 Google Scholar
  • 7. Bouton, C.L. (1901). ‘Nim, a game with a complete mathematical theory’. The Annals of Mathematics. 3, 1/4, 35-39 Google Scholar
  • 8. Burch, J. , Clarke, E. , McMillan, K. , Dill, D. , Hwang, L. (1992). ‘Symbolic model checking: 1020 states and beyond’. Information and Computation. 98, 2, 142-170 Google Scholar
  • 9. Chomsky, N. (1962). Context-free Grammars and Pushdown Storage. MIT Research Lab. Elect, 187-194, in Quarterly Progress Report No. 65 Google Scholar
  • 10. Corbett, J.C. , Dwyer, M.B. , Hatcliff, J. , Laubach, S. , Pasareanu, C.S. , Zheng, H. , et al. (2000). ‘Bandera: extracting finite-state models from Java source code’. in Software Engineering, Proceedings of the International Conference on. IEEE, 439-448 Google Scholar
  • 11. David, A. , Grunnet, J. , Jessen, J. , Larsen, K. , Rasmussen, J. (2012). ‘Application of model-checking technology to controller synthesis’. in Formal Methods for Components and Objects. Springer, 336-351, Vol. 6957 of LNCS Google Scholar
  • 12. Flanagan, C. , Qadeer, S. (2002). ‘Predicate abstraction for software verification’. SIGPLAN Notices. 37, 1, 191-202 Google Scholar
  • 13. Havelund, K. (1999). ‘Java PathFinder, a translator from Java to Promela’. in Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science. Springer, 152 Google Scholar
  • 14. Holzmann, G.J. (1997). ‘State compression in SPIN: recursive indexing and compression training runs’. in Proc. of the 3nd International SPIN Workshop. Google Scholar
  • 15. Ivančić, F. , Yang, Z. , Ganai, M. , Gupta, A. , Ashar, P. (2008). ‘Efficient SAT-based bounded model checking for software verification’. Theoretical Computer Science. 404, 3, 256-274 Google Scholar
  • 16. Jessen, J. , Rasmussen, J. , Larsen, K. , David, A. (2007). ‘Guided controller synthesis for climate controller using UPPAAL TIGA’. in Proc. of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS ‘07), Lecture Notes in Computer Science. 4763, Springer, 227-240 Google Scholar
  • 17. Laarman, A. , Pol, J. , Weber, M. (2011). ‘Parallel recursive state compression for free’. in Proc. of the 18th International SPIN Workshop, Lecture Notes in Computer Science. 6823, Springer, 38-56 Google Scholar
  • 18. Lime, D. , Roux, O. , Seidner, C. , Traonouez, L. (2009). ‘Romeo: a parametric model-checker for Petri nets with stopwatches’. in Tools and Algorithms for the Construction and Analysis of Systems, 15th Int. Conference, TACAS, Springer, 54-57, Vol. 5505 of LNCS Google Scholar
  • 19. Miremadi, S. , Akesson, K. , Fabian, M. , Vahidi, A. , Lennartson, B. (2008). ‘Solving two supervisory control benchmark problems using supremica’. in the 9th Int. Workshop on Discrete Event Systems (WODES ‘08), IEEE, 131-136 Google Scholar
  • 20. Moor, T. , Schmidt, K. , Perk, S. (2010). ‘Applied supervisory control for a flexible manufacturing system’. in 11th Int. Workshop on Discrete Event Systems (WODES ‘10), IFAC/Elsevier, 253-258 Google Scholar
  • 21. Oettinger, A.G. (1961). ‘Automatic syntactic analysis and the pushdown store’. in Structure of Language and its Mathematical Aspects. American Mathematical Society, 104-129, Vol. 12 of Symposia on Applied Mathematics Google Scholar
  • 22. Păsăreanu, C.S. , Mehlitz, P.C. , Bushnell, D.H. , Gundy-Burlet, K. , Lowry, M. , Person, S. , Pape, M. (2008). ‘Combining unit-level symbolic execution and system-level concrete execution for testing NASA software’. in Proc. of the Int. Symposium on Software Testing and Analysis, ISSTA. ACM Press, 15-26 Google Scholar
  • 23. Ramadge, P.J. , Wonham, W.M. (1987). ‘Supervisory control of a class of discrete event processes’. SIAM Journal on Control and Optimization. 25, 1, 206-230 Google Scholar
  • 24. Sistla, A. , Godefroid, P. (2004). ‘Symmetry and reduced symmetry in model checking’. ACM Transactions on Programming Languages and Systems (TOPLAS). 26, 4, 702-734 Google Scholar
  • 25. Zareiee, M. , Dideban, A. , Orouji, A. , Alla, H. (2012). ‘A simple Petri net controller in discrete event systems’. 14, in 14th IFAC Symposium on Information Control Problems in Manufacturing, 188-193 Google Scholar
  • 26. Zhang, Y. , Bérard, B. , Kordon, F. , Thierry-Mieg, Y. (2010). ‘Automated controllability and synthesis with hierarchical set decision diagrams’. in Proc. of the 11th Int. Workshop on Discrete Event Systems (WODES). IFAC/Elsevier, 291-296 Google Scholar
  • 27. Zhang, Y. , Bérard, B. , Hillah, L.M. , Kordon, F. , Thierry-Mieg, Y. (2011). ‘Modeling complex systems with VeriJ’. in Proc. of the 5th Int. Workshop on Verification and Evaluation of Computer and Communication System (VECOS). British Computer Society, 34-45 Google Scholar
  • 28. Zhang, Y. (2010). ‘Modeling automated highway systems with VeriJ’. in Modelling and Verifying Parallel Processes (MOVEP ‘10). 138-143 Google Scholar