As discrete-event systems grow in complexity across domains such as manufacturing, communication, and cyber-physical systems, their modeling and simulation face increasing challenges. Key issues include model reusability, interoperability across heterogeneous simulation platforms, and maintaining consistency of execution semantics. Traditional approaches often rely on simulators bound to specific programming languages, which restricts portability and hinders collaboration across different tools. To overcome these limitations, this paper introduces FPDEVSML, a formal specification language for parallel-DEVS (PDEVS) models. FPDEVSML provides a structured and unambiguous framework for defining system behavior independently of any particular simulator. This language is based on formal foundations in mathematical logic, algebra, and set theory that ensure only well-formed models can be expressed and validated. From a given specification, models are automatically parsed, semantically analyzed, and transformed into a platform-independent representation, which is then used to generate executable code for multiple simulation environments following model-driven engineering (MDE) approach. We demonstrate this approach through the ft4devs (Formal Tool for DEVS) framework, which we developed, providing code generation for both Artis*/C++ and PyPDEVS/Python. Case studies highlight the FPDEVSML language’s expressiveness in modeling parallel and modular systems. The results confirm the feasibility of the approach, bridging the gap between formal modeling and practical simulation for PDEVS modeling formalism, and paving the way for future automatic integration with formal verification.
ZhuFYaoYLiJ, et al. Reusability and composability analysis for an agent-based hierarchical modelling and simulation framework. Simul Model Pract Theory2019; 90: 81–97. https://doi.org/10.1016/j.simpat.2018.10.009
ZeiglerBPVahieS. DEVS formalism and methodology: unity of conception/diversity of application. In: Proceedings of the 1993 winter simulation conference (WSC’93), 1993, pp.573–579. IEEE. https://doi.org/10.1109/WSC.1993.718101
4.
ZeiglerBPrähoferHKimTG. Theory of modeling and simulation. 2nd ed.Academic Press, 2000.
5.
WainerG. Discrete-event modeling and simulation: a practitioner’s approach (Computational analysis, synthesis, and design of dynamic systems). CRC Press, 2009.
6.
CondetteFRamatESondiP. A discrete event approach to micro-scale traffic modeling in urban environment. Simul Model Pract Theory2024; 133: 102920. https://doi.org/10.1016/j.simpat.2024.102920
7.
ChowACHZeiglerBP. Parallel DEVS: a parallel, hierarchical, modular modeling formalism. In: Proceedings of the winter simulation conference, Lake Buena Vista, FL, 11–14 December, pp.716–722. IEEE. https://doi.org/10.1109/WSC.1994.717419
8.
ZeiglerBPMuzyAKofmanE. Theory of modeling and simulation: discrete event & iterative system computational foundations. 3rd ed.Academic Press, 2018.
9.
FranceschiniRBisgambigliaPATourailleL, et al. A survey of modelling and simulation software frameworks using discrete event system specification. In: Proceedings of the 2014 Imperial College computing student workshop, London, 25–26 September, pp.40–49. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2014.
10.
VangheluweH. DEVS as a common denominator for multi-formalism hybrid systems modelling. In: VargaA (ed.) IEEE international symposium on computer-aided control system design. IEEE Computer Society Press, 2000, pp.129–134.
11.
QassoudHAubinBSWainerG, et al. Enabling collaborative modeling through a web library of DEVS models. In: Proceedings of the 2022 annual modeling and simulation conference (ANNSIM), San Diego, CA, 18–20 July 2022, pp.814–823. IEEE. https://doi.org/10.23919/ANNSIM55834.2022.9859291
12.
SarjoughianHSZeiglerBP. Towards making modeling & simulation into a discipline. Simul Ser2001; 33: 130–135.
13.
Risco-MartínJLMittalSFabero JiménezJC, et al. Reconsidering the performance of DEVS modeling and simulation environments using the DEVStone benchmark. Simulation2017; 93: 459–476.
14.
GoreRDialloS. The need for usable formal methods in verification and validation. In: Proceedings of the 2013 winter simulation conference (WSC), Washington, DC, 8–11 December 2013, pp.1257–1268. IEEE.
15.
KhlifiOMosbahiOKhalguiM, et al. GR-TNCES: new extensions of R-TNCES for modelling and verification of flexible systems under energy and memory constraints. In: Proceedings of the 10th international joint conference on software technologies (ICSOFT), Colmar, Alsace, France, 20–22 July 2015.
16.
BatchoudiGFoucherC and Ramat É. Parallel-DEVS specification language for modeling: mathematical approach and grammar. In: 2025 annual modeling and simulation conference (ANNSIM), Madrid, 26–29 May, pp.1–13. IEEE.
17.
KentS. Model driven engineering. In: International conference on integrated formal methods, Turku, 15–17 May 2002, pp.286–298. Springer.
18.
TraoréMK. Combining DEVS and logic. In: Proceedings of the open international conference on modelling and simulation (OICMS), Clermont-Ferrand, 13–15 June 2005, pp.307–317. https://api.semanticscholar.org
19.
van LamsweerdeA. Formal specification: a roadmap. In: Proceedings of the conference on the future of software engineering, Limerick, Ireland, 4–11 June 2000, pp.147–159. ACM Press.
20.
ClarkeEMWingJM. Formal methods: state of the art and future directions. ACM Comput Surv1996; 28: 626–643.
21.
GaudelMC. Formal specification techniques. In: Proceedings of the 16th international conference on software engineering, Washington, DC, 16–21 May 1994, pp.223–227. IEEE.
22.
LanoK. The B language and method: a guide to practical formal development. Springer Science & Business Media, 2012.
23.
ISO/IEC. Information technology—Z formal specification notation—Syntax, type system and semantics. Citeseer, 2002.
24.
MaïgaO. An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems. PhD Thesis, Université Blaise Pascal—Clermont-Ferrand II, 2015.
25.
AlmeidaJBFradeMJPintoJS, et al. (eds) An overview of formal methods tools and techniques. In: Rigorous software development: An introduction to program verification. Springer, 2011, pp.15–44.
26.
de MatosECB. Beta: A b-based testing approach, 2016.
27.
RoggenbachM. CSP-CASL—A new integration of process algebra and algebraic specification. Theor Comput Sci2006; 354: 42–71.
28.
BlasMJGonnetSZeiglerBP. Towards a universal representation of DEVS: a metamodel-based definition of DEVS formal specification. In: 2021 Annual modeling and simulation conference (ANNSIM), Fairfax, VA, 19–22 July 2021, pp.1–12. IEEE.
29.
TraoréMIghorojeUMaïgaO. The DEVS-driven modeling language: syntax and semantics definition by meta modeling and graph transformation. Simul Ser2012; 44: 1–6.
30.
BlasMJGonnetSKimD, et al. A context-free grammar for generating full classic DEVS models. In: Proceedings of the winter simulation conference (WSC’23), San Antonio, TX, 10–13 December 2023, pp.2579–2590. IEEE.
31.
HongKJKimTGKwonIS. Devsif: relational algebraic DEVS intermediate format. In: Proceedings of AIS'2000, AIS, 2000, pp. 83–88.
32.
HongKJKimTG. DEVSpecL: DEVS specification language for modeling, simulation and analysis of discrete event systems. Inf Softw Technol2006; 48: 221–234. https://doi.org/10.1016/j.infsof.2005.04.008
33.
PreyserFHeinzlBRaichP. Towards extending the parallel-DEVS formalism to improve component modularity. In: Workshop der ASIM/GI-Fachgruppen STS und GMMS, Lippstadt, m10–11 March 2016.
34.
MittalSDouglassS. Devsml 2.0: the language and the stack. International Spring Simulation Multi conference, Orlando, FL, 26–29 March 2012.
35.
HollmannDACristiáMFrydmanC. CML-DEVS: a specification language for DEVS conceptual models. Simul Model Pract Theory2015; 57: 100–117. https://doi.org/10.1016/j.simpat.2015.06.007
36.
KalyanasundaramPUgaleSP. Model transformation: concept, current trends and challenges. Int J Comput Appl2015; 119(14).
37.
BézivinJBüttnerFGogollaM, et al. Model transformations? transformation models! In: International conference on model driven engineering languages and systems, Genova, Italy, 1–6 October 2006, pp.440–453. Springer.
38.
LucioLZhangQNguyenPH, et al. Advances in model-driven security. Adv Comput2014; 93: 103–152.
39.
TourailleL. Application of model-driven engineering and metaprogramming to DEVS modeling & simulation. PhD Thesis, Université Blaise Pascal—Clermont-Ferrand II, 2012.
40.
Van TendelooYVangheluweH. Extending the DEVS formalism with initialization information. ArXiv: abs/1802.04527, 2018.
Van TendelooYVangheluweH. The modular architecture of the Python (P) DEVS simulation kernel (WIP). In: Proceedings of the symposium on theory of modeling & simulation—DEVS integrative, Vol. 14, 13–16 April 2014, pp. 387–392. Society for Computer Simulation International.
45.
BarrettCStumpATinelliC. The smt-lib standard: Version 2.0. Technical report, SMT-LIB Initiative, 2010. http://www.smtlib.org
de MouraLBjørnerN. Z3: an efficient SMT solver. In: GaravelHHatcliffJ (eds) Tools and algorithms for the construction and analysis of systems. Springer, 2008, pp.337–340.
