2000 · 76 citations · 15 references
ComputingComputer EngineeringComputer ScienceEmbedded SystemsFormal MethodsReal-time SystemsDeductive VerificationEmbedded Systems DesignModel CheckingPetri NetsReal-time Systems DesignVerificationComputation Tree LogicComputational Tree LogicEmbedded System VerificationFormal VerificationPetri Net Model CheckingPetri Net SemanticsPetri Net VerificationTimed Model Checking
Embedded systems increasingly combine complex hardware and software, making verification of their correctness challenging. The authors propose a Petri net–based model, PRES+, to represent embedded systems and develop new verification methods that address limitations of traditional techniques. They employ model checking of CTL and TCTL properties on PRES+ models to formally prove system correctness. An ATM server case study demonstrates the practical feasibility of the approach.
The ever increasing complexity of embedded systems consisting of hardware and software components poses a challenge in verifying their correctness. New verification methods that overcome the limitations of traditional techniques and, at the same time, are suitable for hardware/software systems are needed. In this work we formally define the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. We introduce an approach to formal verification of such systems: we make use of model checking to prove the correctness of embedded systems by determining the truth of CTL (Computation Tree Logic) and TCTL (Timed CTL) formulas that specify required properties with respect to a PRES+ model. An ATM server illustrates the feasibility of our approach on practical applications.
15
The algorithmic analysis of hybrid systems
Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs et al. · Theoretical Computer Science · 1995 · 1.9K citations · Full text
Model-checking for real-time systems
Rajeev Alur, Costas Courcoubetis, David L. Dill · 2002 · 894 citations