Model checking embedded system designs

It is common knowledge in Information Technology (IT) that an embedded system is based on microprocessor and is built to control a function or a range of functions. Although, it is not designed to be programmed by the end user in the same way that a PC is, it is designed to perform one particular task with choices and different options [1-5]. Multitasking is a method by which multiple tasks, also known as processes, share common processing resources, such as CPU. The main aim of this paper is analysis of the design of the embedded systems and a focus on mid-level abstractions for concurrent programs.

Download Full-text

Efficient Bounded Model Checking for LTL

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.380-384.1239 ◽

2013 ◽

Vol 380-384 ◽

pp. 1239-1242

Author(s):

Rui Wang ◽

Xian Jin Fu

Keyword(s):

Model Checking ◽

Efficient Method ◽

Bounded Model Checking ◽

Specification Languages ◽

Model Checker ◽

System Designs

Bounded Model Checking is an efficient method of finding bugs in system designs. LTL is one of the most frequently used specification languages in model checking. In this paper, We present an linearization encoding for LTL bounded model checking. We use the incremental SAT technology to solve the BMC problem. We implement the new encoding in NuSMV model checker.

Download Full-text

Integrated State Space Reduction for Model Checking Executable Object-Oriented Software System Designs

Fundamental Approaches to Software Engineering - Lecture Notes in Computer Science ◽

10.1007/3-540-45923-5_5 ◽

2002 ◽

pp. 64-79 ◽

Cited By ~ 10

Author(s):

Fei Xie ◽

James C. Browne

Keyword(s):

Model Checking ◽

State Space ◽

Object Oriented ◽

Software System ◽

Space Reduction ◽

System Designs ◽

State Space Reduction

Download Full-text

Observer Patterns for Timed Properties

International Journal of Software Innovation ◽

10.4018/ijsi.2021040101 ◽

2021 ◽

Vol 9 (2) ◽

pp. 1-17

Author(s):

Djamila Baroudi ◽

Safia Nait-Bahloul

Keyword(s):

Model Checking ◽

Embedded System ◽

Formal Methods ◽

Reachability Analysis ◽

Domain Specific Language ◽

Formal Specifications ◽

Specific Language ◽

Domain Specific ◽

Formal Techniques ◽

Timed Properties

Dwyer et al. proposed qualitative specification patterns that enable the practitioners of model checking tools to write formal specifications mainly used for automatic model checking. Although this involves formalisms that are not always easy to handle by engineers, to facilitate the integration of formal methods based on these definition patterns in the industrial field, several formal techniques and languages have been proposed. This paper studies a domain specific language named CDL which help non-experts writing formal specifications effortlessly. In CDL, a property is transformed into an observer automaton to perform a reachability analysis. The existing CDL patterns allow non-experts to reason about occurrence and order of events, but not enough about their timing. Furthermore, the semantics of patterns and transformations are not ideally formalized and are still complex. This work serves to extend the existing CDL system by patterns related to time. The contribution is illustrated in an industrial embedded system.

Download Full-text