scholarly journals Case studies of model checking for embedded system designs

2004 ◽  
Author(s):  
Xi Chen ◽  
H. Hsieh ◽  
F. Balarin ◽  
Y. Watanabe
Keyword(s):  
Model Checking ◽  
Embedded System ◽  
Case Studies ◽  
System Designs

Formal Verification for Embedded System Designs

2003 ◽  
Vol 8 (2/3) ◽  
pp. 139-153 ◽  
Author(s):  
Xi Chen ◽  
Harry Hsieh ◽  
Felice Balarin ◽  
Yosinori Watanabe
Keyword(s):  
Embedded System ◽  
Formal Verification ◽  
System Designs

scholarly journals Multitasking in Embedded System Designs

2019 ◽  
Vol 15 (09) ◽  
pp. 44 ◽  
Author(s):  
Radoslav Mavrevski ◽  
Metodi Traykov ◽  
Iavn Trenchev
Keyword(s):  
Information Technology ◽  
Embedded Systems ◽  
Embedded System ◽  
Common Knowledge ◽  
Concurrent Programs ◽  
End User ◽  
Multiple Tasks ◽  
Range Of Functions ◽  
Processing Resources ◽  
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.

Efficient Bounded Model Checking for LTL

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.

Sign in / Sign up

Export Citation Format

Share Document