5,315 research outputs found
SMT-based bounded model checking of multi-threaded software in embedded systems
No full textOur reliance on the correct functioning of embedded systems is growing rapidly. Such systems are used in a wide range of applications such as airbag control systems, mobile phones, and high-end television sets. These systems are becoming more and more complex and require multi-core processors with scalable shared memory to meet the increasing computational power demands. The reliability of the embedded (distributed) software is thus a key issue in the system development. In this thesis we describe and evaluate an approach to reason accurately and effectively about large embedded software using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT) techniques. We present three major novel contributions. First, we extend the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions and pointers and thus making our approach suitable to reason about embedded software. We then provide new encodings into existing SMT theories and we show that our translations from ANSI-C programs to SMT formulas are as precise as bit-accurate procedures based on Boolean Satisfiability. Second, we develop three related approaches for model checking multi-threaded software in embedded systems. In the lazy approach, we generate all possible interleavings and call the SMT solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the SMT solvers. Finally, we describe and evaluate an approach to integrate our SMT-based BMC into the software engineering process by making the verification process incremental. In particular, our approach looks at the modifications suffered by the software system since its last verification, and submits them to a partly static and dynamic verification process, which is thus guided by a set of test cases for coverage. Experiments show that our SMT-based BMC can analyze larger problems and reduce the verification time compared to state-of-the-art techniques that use BMC, iterative context-bounding or counterexample-guided abstraction refinement
Verifying multi-threaded software using SMT-based context-bounded model checking
No full textWe describe and evaluate three approaches to model check multi-threaded software with shared variables and locks using bounded model checking based on Satisfiability Modulo Theories (SMT) and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the SMT solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we bound the number of context switches allowed among threads in order to reduce the number of interleavings explored. We implemented these approaches in ESBMC, our SMT-based bounded model checker for ANSI-C programs. Our experiments show that ESBMC can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that use iterative context-bounding algorithms or counter-example guided abstraction refinement
Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
No full textEmbedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood
SMT-based bounded model checking for embedded ANSI-C software
No full textPropositional bounded model checking has been applied successfully to verify embedded software but remains limited by increasing propositional formula sizes and the loss of high-level information during the translation preventing potential optimizations to reduce the state space to be explored. These limitations can be overcome by encoding high-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we propose the application of different background theories and SMT solvers to the verification of embedded software written in ANSI-C in order to improve scalability and precision in a completely automatic way. We have modified and extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded software applications from telecommunications, control systems, and medical devices. The experiments show that our ESBMC model checker can analyze larger problems than existing tools and substantially reduce the verification time
Context-bounded model checking of LTL properties for ANSI-C software
No full textContext-bounded model checking has successfully been used to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages like ANSI-C. In this paper, we describe and experiment with an approach to extend context-bounded model checking to liveness properties expressed in linear-time temporal logic (LTL). Our approach converts the LTL formulae into Buechi-automata and then further into C monitor threads, which are interleaved with the execution of the program under test. This combined system is then checked using the ESBMC model checker. Since this approach explores a larger number of interleavings than normal context-bounded model checking, we use a state hashing technique which substantially reduces the number of redundant interleavings that are explored and so mitigates state space explosion. Our experimental results show that we can verify non-trivial properties in the firmware of a medical device
Towards A Semiformal Development Methodology for Embedded Systems
No full textIn recent days, the amount of functions has increased significantly in embedded products so that systems development methodologies play an important role to ensure the product’s quality, cost, and time. Furthermore, this complexity coupled with constantly evolving specifications, has led to propose a semiformal development methodology to support the building of embedded real-time systems. A platform-based design approach has been used to balance costs and time-to-market in relation to performance and functionality constraints. We performed three expressive case studies and we concluded that the proposed methodology significantly reduces design time and improves software modularity and reliability
Bounded Model Checking of Multi-threaded Software using SMT solvers
No full textThe transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the BMC procedure on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation-widening approach, we reduce the state space by abstracting the number of state variables and interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we use partial-order reduction (POR) techniques to reduce the number of interleavings explored. Experiments show that our approaches can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that combine classic POR methods with symbolic algorithms and others that implement the Counter-Example Guided Abstraction Refinement technique
Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking
No full textThe complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In this context, SAT-based bounded model checking has been successfully applied to discover subtle errors, but for larger applications, it often suffers from the state space explosion problem. This paper describes a new approach called continuous verification to detect design errors as quickly as possible by looking at the Software Configuration Management (SCM) system and by combining dynamic and static verification to reduce the state space to be explored. We also give a set of encodings that provide accurate support for program verification and use different background theories in order to improve scalability and precision in a completely automatic way. A case study from the telecommunications domain shows that the proposed approach improves the error-detection capability and reduces the overall verification time by up to 50%
Gift Young Engineers: An Extra-Curricular Initiative for Updating Computer and Electrical Engineering Courses
No full textThe curricula of engineering courses are well defined by the central government for all Brazilian universities. Indeed, there are some mandatory determinations that must be fulfilled prior to the accreditation of any engineering course in Brazil. Modifications must be submitted for evaluation beforehand, resulting in a process that sometimes takes years to be approved. That is a secure way to guarantee that the fundamentals of each engineering program will be part of the students’ carrier all over the country, and at the same time a problem when you need to introduce new technological subjects. That poses a problem when you have new demands for technological curricular components that could express the actual state of the art of modern subjects. Trying to solve these issues some professors from the Federal University of Amazonas developed a flexible extra-curricular program for electrical and computer engineering courses, named Gift Young Engineers. This paper describes the philosophy of these extra-curricular programs. Some examples of successful particular partnerships are also discussed. Indeed the proposed training programs for Digital TV Systems (hardware and software) will be presented and analyzed in details. The obtained results will also be discussed in order to contribute to similar experiences worldwide
Context-bounded model checking with ESBMC 1.17
Full text linkESBMC is a context-bounded symbolic model checker that allows the verification of single- and multi-threaded C code with shared variables and locks. ESBMC supports full ANSI-C, and can verify programs that make use of bit-level operations, arrays, pointers, structs, unions, memory allocation and floating-point arithmetic. It can reason about arithmetic under- and overflows, pointer safety, memory leaks, array bounds violations, atomicity and order violations, local and global deadlocks, data races, and user-specified assertions. However, as other bounded model checkers, ESBMC is in general incomplete
- …
