Research PaperNo Access

Formal verification with HiLLS-specified models: A further step in multi-analysis modeling of complex systems

Kehinde G. Samuel

African University of Science & Technology, Abuja, Nigeria

E-mail Address: keliake@aust.edu.ng

Search for more papers by this author

Oumar Maiga

Université des Sciences des Techniques et des Technologies Bamako, Mali

E-mail Address: oumary.maiga@usttb.edu.ml

Search for more papers by this author

, and

Mamadou K. Traoré

University of Bordeaux, IMS CNRS UMR 5218, France

E-mail Address: mamadou-kaba.traore@u-bordeaux.fr

Corresponding author.

Search for more papers by this author

https://doi.org/10.1142/S1793962319500326Cited by:3 (Source: Crossref)

Abstract

The multi-analysis modeling of a complex system is the act of building a family of models which allows to cover a large spectrum of analysis methods (such as simulation, formal methods, enactment, $\dots$ $\dots$ ) that can be performed to derive various properties of this system. The High-Level Language for Systems Specification (HiLLS) has recently been introduced as a graphical language for discrete event simulation, with potential for other types of analysis, like enactment for rapid system prototyping. HiLLS defines an automata language that also opens the way to formal verification. This paper provides the building blocks for such a feature. That way, a unique model can be used not only to perform both simulation and enactment experiments but also to allow the logical analysis of properties without running any experiment. Therefore, it saves from the effort of building three different analysis-specific models and the need to align them semantically.

Keywords:

References

1. Hong K. J., Kim T. G., DEVSpecL: DEVS specification language for modeling, simulation, and analysis of discrete event systems, Inform. Softw. Technol. 48 :221–234, 2006. Web of Science, Google Scholar
2. Estefan J. A., Survey of Model-Based Systems Engineering (MBSE) Methodologies, INCOSE MBSE Focus Group, Vol. 25, 2007. Google Scholar
3. Finkelstein A., Kramer J., Nuseibeh B., Finkelstein L., Goedicke M., Viewpoints: A framework for integrating multiple perspectives in system development, Int. J. Softw. Eng. Knowled. Eng. 2 :31–57, 1992. Link, Web of Science, Google Scholar
4. Kurpjuweit S., Winter R., Viewpoint-based Meta model engineering. EMISA2007, Ges. für Informatik, Bonn, pp. 143–159, 2007. Google Scholar
5. Gianni D., D’Ambrogio A., Tolk A., Modeling and Simulation-Based Systems Engineering Handbook, CRC Press, 2014, ISBN 978-1-4665-7145-7. Google Scholar
6. Zeigler B. P., Theory of Modeling and Simulation, 1st edn., Academic Press, 1976. Google Scholar
7. Zeigler B. P., Praehofer H., Kim T. G., Theory of Modeling and Simulation: Integrating Discrete Event and Continuous Complex Dynamic Systems, Academic Press, 2000. Google Scholar
8. Zeigler B. P., Muzy A., Kofman E., Theory of Modeling and Simulation: Discrete Event & Iterative System Computational Foundations, Academic Press, 2018. Google Scholar
9. Maïga, An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems, Ph.D. Thesis, Université Blaise Pascal — Clermont-Ferrand II, 2015. Google Scholar
10. Aliyu H. O., An integrative framework for model-driven systems engineering: Towards the co-evolution of simulation, formal analysis and enactment methodologies for discrete event systems, Ph.D. Thesis in Computer Science, Université Blaise Pascal — Clermont-Ferrand II, December 2016. Google Scholar
11. Aliyu H. O., Maïga O., Traoré M. K., The high-level language for systems specification: A model-driven approach to systems engineering, Int. J. Model. Simul. Sci. Comput. 7 :1641003, 2016. Link, Google Scholar
12. Aliyu H. O., Maïga O., Traoré M. K., A framework for discrete event systems enactment. Proc. 29th European Simulation and Modeling Conf. ISBN: 978-9077381-908, EUROSIS-ETI, pp. 149–156, 2015. Google Scholar
13. M. K. Traoré, Combining DEVS and Logic, OICMS, Blaise Pascal University, pp. 307–317, 2005. Google Scholar
14. Dr. Anastasia-Maria Leventi-Peetz, Summary of the Book: Formal Methods for Safe and Secure Computer Systems, Federal Office for Information Security, 2013. Google Scholar
15. Dacharry H., Giambiasi N., Formal verification with timed automata and DEVS models: A case study, Proc. ASSE’05, Argentine Society for Computer Science and Operational Research, Rosario, pp. 251–269, August 29, 2005. Google Scholar
16. Dacharry H. P., Giambiasi N., A formal verification approach for DEVS, Proc. 2007 Summer Computer Simulation Conf., San Diego, California, pp. 312–319, 2007. Google Scholar
17. Furfaro A., Nigro L., A development methodology for embedded systems based on RT-DEVS, Innov. Syst. Softw. Eng. 5 :117–127, 2009. Google Scholar
18. Hong, J. S., and Kim, T. G., 1997. Real-time discrete event system specification formalism for seamless real-time software development, Discrete Event Dyn. Syst. Theory Appl. 7 :355–375, 1997. Web of Science, Google Scholar
19. Cicirelli F., Furfaro A., Nigro L., Pupo F., Temporal verification of RT-DEVS models with implementation aspects, Proc. 2010 Spring Simulation Multiconf., Society for Computer Simulation International, 2010. Google Scholar
20. Saadawi H., Wainer G., Verification of real-time DEVS models, Proc. 2009 Spring Simul. Multiconf., Society for Computer Simulation International, San Diego, CA, USA, p. 143, March 22–27, 2009. Google Scholar
21. Madlener F., Weingart J., Huss S. A., Verification of dynamically reconfigurable embedded systems by model transformation rules, 4th IEEE/ACM Int. Conf. Hardware-Software Codesign and System Synthesis (CODES+ISSS 2010), Scottsdale, Arizona, USA, October 24–29, 2010. Google Scholar
22. Zeigler B. P., Nutaro J. J., Seo C., Combining DEVS and model-checking: Concepts and tools for integrating simulation and analysis, Int. J. Simul. Process Model. Vol. 12, pp. 2–15, 2017. Google Scholar
23. Zeigler B. P., Sarjoughian H. S., Guide to Modeling and Simulation of Systems of Systems, Springer, 2012. Google Scholar
24. Kuhn D. R., Craigen D., Saaltink M., Practical application of formal methods in modeling and simulation, Summer Computer Simulation Conf., Society for Computer Simulation International, Montreal, Quebec, Canada, pp. 726–731, July 20–24, 2003. Google Scholar
25. Traoré M. K., Making DEVS models amenable to formal analysis, Symp. Theory of Modeling & Simulation: DEVS Integrative M&S Symp., Huntsville, Alabama, USA, 6 pp, Society for Computer Simulation International, April 2–6 2006. Google Scholar
26. Trojet W., Berradia T., 2015. System Reliability using Simulation Models and Formal Methods. Int. J. Comput. Appl. 132 :1–8. Google Scholar
27. Yacoub A., Hamri M., Frydman C., A method for improving the verification and validation of systems by the combined use of simulation and formal methods, IEEE/ACM 18th Int. Symp. Distributed Simulation and Real-Time Applications, Toulouse, France, pp. 155–162, October 1–3, 2014. Google Scholar
28. Lano K., Clark D., Androutsopoulos K., UML to B: Formal Verification of Object-Oriented Models. Integrated Formal Methods, Springer, Berlin, Heidelberg, pp. 187–206, 2004. Google Scholar
29. Lilius J., Paltor I. P., vUML: A tool for verifying UML models, 14th IEEE Int. Conf. Automated Software Engineering, Cocoa Beach, FL, USA, pp. 255–258, October 12–15, 1999. Google Scholar
30. Shah S. M., Anastasakis K., Bordbar B., From UML to Alloy and Back Again. Models in Software Engineering, Springer, Berlin, Heidelberg, pp. 158–171, 2009. Google Scholar
31. Laleau R., Semmak F., Matoussi A., Petit D., Hammad A., Tatibouet B., A First Attempt to Combine SysML Requirements Diagrams and B. Innov. Syst. Softw. Eng. 6 :47–54, 2010. Google Scholar
32. Kapos G.-D., Dalakas V., Nikolaidou M., Anagnostopoulos D., An integrated framework for automated simulation of SysML models using DEVS, Simulation 90 :717–744, 2014. Google Scholar
33. Risco-Martín J. L., Jesús M., Mittal S., Zeigler B. P., eUDEVS: Executable UML with DEVS Theory of Modeling and Simulation. Simulation 85 :750–777, 2009. Google Scholar
34. Schamai W., Fritzson P., Paredis C., Pop A., Towards unified system modeling and simulation with ModelicaML: Modeling of executable behavior using graphical notations, 7th Int. Modelica Conf., Linköping University Electronic Press, pp. 612–621, 2009. Google Scholar
35. Shaikh R., Vangheluwe H., Transforming UML2.0 class diagrams and Statecharts to Atomic DEVS, Symposium on Theory of Modeling & Simulation: DEVS, Boston, Massachusetts — April 3–07, 2011, Society for Computer Simulation International, San Diego, CA, USA, pp. 205–212, 2011. Google Scholar
36. Zeigler B. P., Traoré M. K., Zacharewicz G., Value-Based Learning Healthcare Systems: Integrative Modeling and Simulation, Institution of Engineering and Technology (The IET Book Series on e-Health Technologies). ISBN: 978-1-78561-326-5, 376 p, 2018b. Google Scholar
37. Maiga O., Hazmat O. A., Mamadou K. T., A new approach to modeling dynamic structure systems, Proc. 2015 European Simulation Modeling Conf. pp. 141–48, https://doi.org/10.1017/CBO9781107415324, 2015. Google Scholar