Abstract
C-DEVS is a formalism for modeling and analysis of discrete event systems. It refers to the original formalism defined by Zeigler in 1976. While the simulation algorithms are well defined, their implementation is a challenge due to both correctness and efficiency issues. This work aims at studying the formalism and its operational semantics. We review and validate the meta-model for SimStudio - a Java implementation of the DEVS simulation protocol, and we debug its existing Java codes. We finally use formal methods to perform model checking and theorem proving on the C-DEVS simulation system to assess the properties of correctness.
DJITOG, I (2021). Formal and Operational Study of C-DEVS. Afribary. Retrieved from https://afribary.com/works/formal-and-operational-study-of-c-devs
DJITOG, IGNACE "Formal and Operational Study of C-DEVS" Afribary. Afribary, 13 Apr. 2021, https://afribary.com/works/formal-and-operational-study-of-c-devs. Accessed 10 May. 2024.
DJITOG, IGNACE . "Formal and Operational Study of C-DEVS". Afribary, Afribary, 13 Apr. 2021. Web. 10 May. 2024. < https://afribary.com/works/formal-and-operational-study-of-c-devs >.
DJITOG, IGNACE . "Formal and Operational Study of C-DEVS" Afribary (2021). Accessed May 10, 2024. https://afribary.com/works/formal-and-operational-study-of-c-devs