کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422472 | 685094 | 2008 | 27 صفحه PDF | دانلود رایگان |

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.
Journal: Electronic Notes in Theoretical Computer Science - Volume 214, 28 June 2008, Pages 131-157