ABSTRACT
We propose a framework for formal analysis of DEVS Driven Modeling Language (DDML) models in order to assess and evaluate the properties of DDML models. This framework semantically maps the hierarchical levels of DDML: Input Output system (IOS), Input Output Relation Observation (IORO) and Coupled Network (CN) levels to corresponding formal methods: Labeled Transition System (LTS), Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and Communicating Sequential Processes (CSP) respectively. These formal methods capture the semantics of DDML at each level of abstraction and we use formal tools (such as JTORX, LTSA, PAT and NUSMV) to automatically analyze these formal specifications to evaluate properties of DDML models at each level.
Ezekiel, S (2021). Formal Analysis Of DDML. Afribary. Retrieved from https://afribary.com/works/formal-analysis-of-ddml
Ezekiel, Soremekun "Formal Analysis Of DDML" Afribary. Afribary, 16 Apr. 2021, https://afribary.com/works/formal-analysis-of-ddml. Accessed 16 Nov. 2024.
Ezekiel, Soremekun . "Formal Analysis Of DDML". Afribary, Afribary, 16 Apr. 2021. Web. 16 Nov. 2024. < https://afribary.com/works/formal-analysis-of-ddml >.
Ezekiel, Soremekun . "Formal Analysis Of DDML" Afribary (2021). Accessed November 16, 2024. https://afribary.com/works/formal-analysis-of-ddml