Real-time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify that kind of temporal properties requires to use something beyond simulation. In this work, we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models, even though Uppaal cannot deal in general with this kind of properties. In order to overcome these limitations, we use the technique known as automata observer. Second, by introducing mutations to quantitative temporal properties, we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented.
CuiYMartinULiangJ.Pulsim: user-based adaptable simulation tool for railway planning and operations. J Adv Transport2018; 2018: 7284815.
2.
ChirkinAMBelloumASKovalchukSV, et al. Execution time estimation for workflow scheduling. Future Gener Comp Syst2017; 75: 376–387.
3.
ZeiglerBPraehoferHKimT.Theory of modeling and simulation: integrating discrete event and continuous complex dynamic systems. Cambridge, MA: Academic Press, 2000, http://books.google.com.uy/books?id=REzmYOQmHuQC
4.
ClarkeEMKlieberWNováčekM, et al. Model checking and the state explosion problem. Berlin: Springer, 2012, pp. 1–30.
5.
HongJSSongHSKimTG, et al. A real-time discrete event system specification formalism for seamless real-time software development. Discrete Event Dynam Syst1997; 7: 355–375.
6.
BehrmannGDavidALarsenKG.A tutorial on Uppaal. In: BernardoMCorradiniF (eds) Formal methods for the design of real-time systems, Vol. 3185. New York: Springer, 2004, pp. 200–236.
7.
SuzukiILuH.Temporal Petri nets and their application to modeling and analysis of a handshake daisy chain arbiter. IEEE Trans Comput1989; 38: 696–704.
8.
MolterHG.Discrete event system specification. In: MolterHG (ed.) SynDEVS co-design flow. New York: Springer, 2012, pp. 9–42.
9.
AlurRDillDL.A theory of timed automata. Theoret Comput Sci1994; 126: 183–235.
PnueliA. The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, RI, 31 October–1 November 1977. New York: IEEE Computer Society, pp. 46–57.
12.
ClarkeEMEmersonEASistlaAP.Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst1986; 8: 244–263.
13.
CimattiAClarkeEMGiunchigliaE, et al. NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification, CAV ’02, Berlin, 27–31 July 2002, pp. 359–364. New York: Springer.
14.
HolzmannGJ.The model checker SPIN. IEEE Trans Softw Eng1997; 23: 279–295.
15.
AlurRCourcoubetisCDillDL. Model-checking for real-time systems. In: Proceedings of the Fifth annual symposium on logic in computer science (LICS ’90), Philadelphia, PA, 4–7 June 1990. New York: IEEE, pp. 414–425.
BackesJDWhalenMWGacekA, et al. On implementing real-time specification patterns using observers. In: RayadurgamSTkachukO (eds.) NASA formal methods. Cham: Springer, pp. 19–33.
20.
AlurR.Techniques for automatic verification of real-time systems. PhD thesis, Stanford University, Stanford, CA, 1992.
21.
GonzalezACristiáMLunaC. Mutants for metric temporal logic formulas. In: MarínBBritoISMoraMK, et al. (eds) Proceedings of the XXII IberoAmerican Conference on Software Engineering, CIbSE 2019, La Habana, Cuba, 22–26 April 2019, pp. 349–362. Newry, Northern Ireland: Curran Associates.
22.
SongHSKimTG.Application of Real-Time DEVS to analysis of safety-critical embedded control systems: railroad crossing control example. SIMULATION2005; 81: 119–136.
23.
FurfaroANigroL. Embedded control systems design based on RT-DEVS and temporal analysis using Uppaal. In: 2008 international multiconference on computer science and information technology, Wisla, 20–22 October 2008, pp. 601–608. New York: IEEE.
24.
CicirelliFFurfaroANigroL. Actor-based simulation of PDEVS systems over HLA. In: 41st annual simulation symposium (anss-41 2008), Ottawa, ON, Canada, 13–16 April 2008, pp. 229–236. New York: IEEE.
25.
DacharryHPGiambiasiN. A formal verification approach for DEVS. In: Proceedings of the 2007 summer computer simulation conference. SCSC ’07, San Diego, CA, 16–19 July 2007, pp. 312–319. New York: ACM.
26.
Inostrosa-PsijasAOyarzún -SilvaMMedina-QuispeF, et al. Verificación formal de un modelo de simulación DEVS de una aplicación Storm. Ingeniare Revista Chilena De Ingeniería2019; 27: 682–695.
27.
ToshniwalATanejaSShuklaA, et al. Storm@twitter. In: Proceedings of the 2014 ACM SIGMOD international conference on management of data, SIGMOD ’14, Snowbird, UT, 22–27 June 2014, pp. 147–156. New York: Association for Computing Machinery.
28.
SaadawiHWainerG.Principles of discrete event system specification model verification. Simulation2013; 89: 41–67.
29.
SaadawiHWainerGMoallemiM.Principles of DEVS model verification for real-time embedded applications. Boca Raton, FL: CRC Press, 2012, pp. 63–96.
30.
GholamiSSarjoughianHS. Modeling and verification of network-on-chip using constrained-DEVS. In: Proceedings of the symposium on theory of modeling & simulation, TMS/DEVS ’17, Virginia Beach, VI, 23–26 April 2017. San Diego, CA: Society for Computer Simulation International.
31.
BüchlerMOudinetJPretschnerA.Security mutants for property-based testing. In: GogollaMWolffB (eds) Tests and proofs, Vol. 6706. New York: Springer, 2011, pp. 69–77.
32.
TanLSokolskyOLeeI.Specification-based testing with linear temporal logic. In: Proceedings of the 2004 IEEE international conference on information reuse and integration, Las Vegas, NV, 8–10 November 2004, pp. 493–498. New York: IEEE.
33.
TrakhtenbrotMB. Mutation patterns for temporal requirements of reactive systems. In: 2017 IEEE international conference on software testing, verification and validation workshops (ICSTW), Tokyo, Japan, 13–17 March 2017, pp.116–121. New York: IEEE.
34.
StocksPCarringtonDA.Test template framework: a specification-based testing case study. In: OstrandTJWeyukerEJ (eds.) Proceedings of the 1993 international symposium on software testing and analysis, ISSTA 1993, Cambridge, MA, 28–30 June 1993, pp. 11–18. New York: ACM.
35.
GonzalezACristiáMLunaC. Error finding in real-time systems using mutants of temporal properties. In: 2021 40th international conference of the Chilean computer science society (SCCC), La Serena, Chile, 15–19 November 2021, pp. 1–8. New York: IEEE.
36.
WainerGAGoldsteinRKhanA. Introduction to the discrete event system specification formalism and its application for modeling and simulating cyber-physical systems. In: 2018 Winter simulation conference (WSC), Gothenburg, 9–12 December, pp. 177–191. New York: IEEE.
37.
BengtssonJYiW.Timed automata: semantics, algorithms and tools. Berlin: Springer, 2004, pp. 87–124.
SaadawiHWainerG. Verification of real-time DEVS models. In: Proceedings of the 2009 spring simulation multiconference, SpringSim ’09, San Diego, CA, 22–27 March. San Diego, CA: Society for Computer Simulation International.
40.
SelicB.The pragmatics of model-driven development. IEEE Softw2003; 20: 19–25.
41.
GonzálezALunaCDanieleM, et al. Towards an automatic model transformation mechanism from UML state machines to DEVS models. CLEI Electron J2015; 18: 334.
42.
GonzálezALunaCDAbellaR. UML state machine as modeling language for DEVS formalism. In: XLII Latin American computing conference, CLEI 2016, Valparaíso, Chile, 14–16 October 2016, pp. 1–12. New York: IEEE, http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7814932
43.
BergeroFKofmanE.PowerDEVS: a tool for hybrid system modeling and real-time simulation. Simulation2011; 87: 113–132.
44.
DwyerMBAvruninGSCorbettJC.Patterns in property specifications for finite-state verification. In: BoehmBWGarlanDKramerJ (eds) Proceedings of the 1999 International Conference on Software Engineering, ICSE’99, Los Angeles, CA, 16–22 May 1999, pp. 411–420. New York: ACM, http://dblp.uni-trier.de/db/conf/icse/icse99.html#DwyerAC99
45.
KonradSChengBHC. Real-time specification patterns. In: Proceedings of the 27th international conference on software engineering. ICSE ’05, St. Louis, MO, 15–21 May 2205, pp. 372–381. New York: ACM.
AbidNDal ZilioSLe BotlanD.Real-time specification patterns and tools. New York: Springer, 2012, pp. 1–15.
48.
OuaknineJWorrellJ. Safety metric temporal logic is fully decidable. In: HermannsHPalsbergJ (eds) Tools and algorithms for the construction and analysis of systems. Berlin: Springer, pp. 411–425.
49.
OuaknineJWorrellJ. Some recent results in metric temporal logic. In: Proceedings of the 6th international conference on formal modeling and analysis of timed systems, FORMATS ’08, Saint Malo, 15–17 September 2008. Berlin: Springer, pp. 1–13.
50.
AcetoLBurgueñoALarsenKG. Model checking via reachability testing for timed automata. In: SteffenB (ed.) Tools and algorithms for the construction and analysis of systems (Lecture notes in computer science), Vol. 1384. New York: Springer, pp. 263–280.
51.
BeerIBen-DavidSChocklerH, et al. Explaining counterexamples using causality. In: BouajjaniAMalerO (eds) Computer aided verification. Berlin: Springer, pp. 94–108.
KaleeswaranAPNordmannAVogelT, et al. A systematic literature review on counterexample explanation. Inform Softw Tech2022; 145: 106800.
54.
LimaLHuertayMuniveJJTraytelD. Explainable online monitoring of metric first-order temporal logic. In: International conference on tools and algorithms for the construction and analysis of systems, Hamilton, ON, Canada, 3–8 May. New York: Springer, pp. 288–307.
55.
HoHMOuaknineJWorrellJ. Online monitoring of metric temporal logic. In: BonakdarpourBSmolkaSA (eds) Runtime verification. Cham: Springer, pp. 178–192.
BouyerPGastinPHerbreteauF, et al. Zone-based verification of timed automata: extrapolations, simulations and what next. In: Formal modeling and analysis of timed systems: 20th international conference, FORMATS 2022, Warsaw, 13–15 September 2022. Berlin: Springer.
58.
BehrmannGBengtssonJDavidA, et al. Uppaal implementation secrets. In: VytopilJ (ed.) Formal techniques in real-time and fault-tolerant systems. Berlin: Springer, pp. 3–22.
59.
LindahlMPetterssonPYiW. Formal design and analysis of a gear controller. In: Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems, TACAS ’98, Lisbon, 28 March–4 April, pp. 281–297. Berlin: Springer.
60.
BowmanHFacontiGKatoenJP, et al. Automatic verification of a lip-synchronisation protocol using Oppaal. Form Asp Comput1998; 10: 550575.
61.
RavnAPSrbaJVighioS. Modelling and verification of web services business activity protocol. In: AbdullaPALeinoKRM (eds) Modelling and verification of web services business activity protocol. Berlin: Springer, pp. 357–371.
62.
BakhshiZRodriguez- NavasGHanssonH. Using UPPAAL to verify recovery in a fault-tolerant mechanism providing persistent state at the edge. In: 2021 26th IEEE international conference on emerging technologies and factory automation (ETFA), Vasteras, 7–10 September 2021. New York: IEEE.
63.
OMG. Meta object facility (MOF) 2.0 query/view/transformation specification, version 1.1, 2011, http://www.omg.org/spec/QVT/1.1/
