Paper Info
Title
SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends.
Abstract
The dependency on the correct functioning of embedded systems is rapidly growing, mainly due to their wide range of applications, such as micro-grids, automotive device control (e.g., airbag control), health care, surveillance, mobile devices, and consumer electronics. Their structures are becoming more and more complex and now require multi-core processors with scalable shared memory, in order to meet increasing computational power demands. As a consequence, reliability of embedded (distributed) software becomes a key issue during system development, which must be carefully addressed and assured. Normally, state-of-the-art verification methodologies for embedded systems generate test vectors (with constraints) and use assertion-based verification and highlevel processor models, during simulation; however, other additional challenges have been raised: the need for meeting time and energy constraints, handling concurrent software, dealing with platform restrictions, evaluating implementation-structure choices, and supporting new software architectures and legacy designs (usually written in low-level languages). The present paper discusses challenges, problems, and recent advances to ensure correctness and timeliness regarding embedded systems. Reliability issues, in the development of micro-grids and cyber-physical systems, are then considered, as a prominent (bounded) model checking application.
Year
Venue
Field
2016
ACM SIGSOFT Software Engineering Notes
Program slicing,Model checking,Software engineering,Shared memory,Computer science,Correctness,Software,Mobile device,Embedded system,Distributed computing,Automotive industry,Scalability
DocType
Volume
Issue
Journal
41
3
Citations 
PageRank 
References 
1
0.37
32
Authors
2
Name
Order
Citations
PageRank
Lucas Cordeiro136038.38
E. B. de Lima Filho24512.51