Welcome to the InfoSci Platform
Reference Hub1
Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language

Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language

Meliouh Amel, Chaoui Allaoua
Copyright: © 2018 |Volume: 6 |Issue: 2 |Pages: 17
ISSN: 2166-7292|EISSN: 2166-7306|EISBN13: 9781522546740|DOI: 10.4018/IJCSSA.2018070103
Cite Article Cite Article

MLA

Amel, Meliouh, and Chaoui Allaoua. "Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language." IJCSSA vol.6, no.2 2018: pp.42-58. http://doi.org/10.4018/IJCSSA.2018070103

APA

Amel, M. & Allaoua, C. (2018). Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language. International Journal of Conceptual Structures and Smart Applications (IJCSSA), 6(2), 42-58. http://doi.org/10.4018/IJCSSA.2018070103

Chicago

Amel, Meliouh, and Chaoui Allaoua. "Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language," International Journal of Conceptual Structures and Smart Applications (IJCSSA) 6, no.2: 42-58. http://doi.org/10.4018/IJCSSA.2018070103

Export Reference

Mendeley
Favorite Full-Issue Download

Abstract

The approach proposed in this article presents a formal verification of embedded systems. The method relies on an automated modeling and code generation based on the systems' behavior. The key concept is the combined use of a subset of UML behavior diagrams extended with timing annotations (Real-Time Statechart and Real-Time Collaboration diagrams) for system modeling and the Maude language for verification. First, UML modeling tools are developed. Then, an automatic generation of equivalent Maude specification is performed. The approach is based on code generation. This is why it is possible to use an available model checking tool to verify certain timed properties represented in Linear Temporal Logic (LTL). The meta-modeling tool ATOM3 is used. A case study is presented to illustrate the feasibility of the approach.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.