System verification is an ever-lasting system engineering challenge. The increasing complexity in system simulation requires some level of expertise in handling the idioms of logic and discrete mathematics to correctly drive a full verification process. It is recognized that visual modeling can help to fill the knowledge gap between system experts and analysis experts. However, such an approach has been used on the one hand to specify the behavior of complex systems, and on the other hand to specify complex requirement properties, but not simultaneously. This paper proposes a framework that is unique in supporting a full system verification process based on the graphical modeling of both the system of interest and the requirements to be checked. Patterns are defined to transform the resulting models to formal specifications that a model checker can manipulate. A real-time crossing system is used to illustrate the proposed framework.
BryantBRGrayJMernikM, et al. Challenges and directions in formalizing the semantics of modeling languages. Comput Sci Inform Syst2011; 8(2): 225–253.
2.
AliyuHOMaïgaOTraoréMK. The high-level language for systems specification: A Model-driven approach to systems engineering. Int J Model Sim Sci Comput2016; 7(1): 1641003.
3.
ZeiglerBP. Theory of Modeling and Simulation. 1st edition. New York: John Wiley & Sons. Inc., 1976.
4.
AliyuHOMaïgaOTraoréMK. A framework for discrete event systems enactment. In: Proceedings of the 29th European Simulation and Modeling Conference -ESM’15, EUROSIS-ETI, Leicester, UK, 2015, pp.149–156.
5.
SamuelKGMaïgaOTraoréMK. Formal verification with HiLLS-specified models: A further step in multi-analysis modeling of complex systems. Int J Model Simulat Sci Comput2019; 10(05): 1950032.
6.
HongKJKimTG. DEVSpecL: DEVS specification language for modeling, simulation, and analysis of discrete event systems. Inform Software Technol2006; 48(4): 221–234.
7.
BüchiJR. On a decision method in restricted second-order arithmetic. In: Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science, NagelE., et al. (Eds.). Stanford University Press, Stanford, CA, 1962, pp.1–11.
8.
ZeiglerBPNutaroJJSeoC. Combining DEVS and model-checking: Concepts and tools for integrating simulation and analysis. Int J Simulat Process Model2017; 12(1): 2–15.
9.
ZeiglerBPSarjoughianHS. Guide to Modeling and Simulation of Systems of Systems. Berlin, Germany: Springer Publication Company, 2012.
10.
FurfaroANigroL. A development methodology for embedded systems based on RT-DEVS. Innovat Syst Software Eng2009; 5(2): 117–127.
11.
SaadawiHWainerG. Verification of real-time DEVS models. In: Proceedings of the 2009 Spring Simulation Multiconference, Society for Computer Simulation International, San Diego, California, United State, 2009, pp.1–8.
12.
MadlenerFWeingartJHussSA. Verification of dynamically reconfigurable embedded systems by model transformation rules. In: Proceedings of IEEE/ACM/IFIP 8th International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS 2010) part of the Embedded Systems Week, Association for Computing Machinery, New York, NY, United States, 2010, pp.33–40. https://doi.org/10.1145/1878961.1878969
13.
MaïgaO. An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems. Ph.D. Thesis, Université Blaise Pascal - Clermont-Ferrand II, France, 2015.
14.
MalerOMannaZPnueliA.From timed to hybrid systems. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop 1992. Springer-Verlag, London, 1992, pp.447–484.
15.
NutaroJ. Toward a theory of superdense time in simulation models. ACM Trans Model Comput Simulat2020; 30(3): Article 16, 13 pages, DOI: https://doi.org/10.1145/3379489.
16.
JouaultFAllilaireFBezivinJ, et al. ATL: A model transformation tool. Sci ComputProgram2008; 72(1–2): 31–39.
17.
BaierCKatoenJP. Principles of Model Checking. Cambridge, Massachusetts London, England: The MIT Press, 2008.
18.
PnueliA. The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS’77), IEEE Computer Society, 1730 Massachusetts Ave., NW Washington, DC, United States, 1977, pp.46–57. https://doi.org/10.1109/SFCS.1977.32
19.
ClarkeEMEmersonEASistlaAP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst1986; 8(2): 244–263.
20.
DwyerMBAvruninGSCorbettJC. Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (ICSE-99), IEEE, Los Angeles, 1999, pp.411–420.
21.
DwyerMBAvruninGSCorbettJC. Property specification patterns for finite-state verification In: FMSP 1998 Proc. 2nd workshop Formal methods in software practice, New York, NY, USA, 1998, pp. 7–15.
KozenD. Results on the Propositional μ-Calculus. Theor Comput Sci1983; 27(3): 33–354.
24.
MeyersBDeshayesRLucioL, et al. ProMoBox: A framework for generating domain-specific property languages. In: 7th International Conference on Software Language Engineering (SLE), Springer, Vasteras, Sweden, 2014, pp.1–20. doi:10.1007/978-3-319-11245-9_1
25.
KleinFGieseHJoint structural and temporal property specification using timed story scenario diagrams. In: Proceedings of the International Conference on Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, 2007, pp.185–199.
BehrmannGDavidALarsenK, et al. UPPAAL 4.0. In: Proceedings of the 3rd International Conference on Quantitative Evaluation of Systems (QEST 2006), IEEE Computer Society, Washington, DC, 2006, pp.125–126.
28.
AlpernBSchneiderFB. Defining liveness. Inform Process Lett1985; 21(4): 181–185.
29.
CallahanJSchneiderFEasterbrookF. Automated software testing using model checking. In: Proceeding of the 1996 SPIN Workshop, Citeseer, Rutgers University, New Brunswick, NJ, 1996, pp.118–127.
