Paper Info
Title
Refinement-Based Verification of Interactive Real-Time Systems
Abstract
Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with system's requirements. To cover this, we integrate a specification framework with a verification system. Given a system, represented in a formal specification framework Focus, one can verify its properties by translating the specification to a Higher-Order Logic and subsequently using the theorem prover Isabelle/HOL. Moreover, using this approach one can validate the refinement relation between two given systems. The approach uses the idea of refinement-based verification: we see any proof about a system as the proof that a more concrete system specification is a refinement of a more abstract one. The case when one needs to prove a single property of a system specification can also be seen as a refinement relation: this property can be defined as a Focus specification itself and then one needs just show that the system specification is its refinement. The major aspects of this approach are exemplified here by a case study on telematics (electronic data transmission) gateway.
Year
DOI
Venue
2008
10.1016/j.entcs.2008.06.007
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
refinement-based verification,system specification,formal specification framework focus,verification system,formal specification,concrete system specification,specification framework,specification problem,refinement,interactive real-time systems,system description,focus specification,verification,real-time systems,automotive gateway,refinement relation,real time systems,higher order logic,theorem prover,natural language,data transmission
Specification language,Programming language,Programming language specification,Computer science,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Refinement,Formal methods,System requirements specification,Formal verification
Journal
Volume
ISSN
Citations 
214,
Electronic Notes in Theoretical Computer Science
8
PageRank 
References 
Authors
0.70
2
1
Name
Order
Citations
PageRank
Maria Spichkova116015.29