Conferences in Research and Practice in Information Technology
  

Online Version - Last Updated - 20 Jan 2012

 

 
Home
 

 
Procedures and Resources for Authors

 
Information and Resources for Volume Editors
 

 
Orders and Subscriptions
 

 
Published Articles

 
Upcoming Volumes
 

 
Contact Us
 

 
Useful External Links
 

 
CRPIT Site Search
 
    

Plug-in Proof Support for Formal Development Environments

Hemer, D., Long, G. and Strooper, P.

    A number of industrial software development standards mandate that safety-critical software components be developed using formal methods, including formal verification. While formal development is supported by a number of formal development environments, verification of correctness properties is still a major bottleneck. Most formal development environments provide built-in facilities for discharging these correctness properties (so-called proof obligations). However these built-in tools are typically less mature and sophisticated than stand-alone theorem provers. FDEs would benefit from being able to use a variety of theorem provers to discharge proof obligations, where different provers can be selected for different problem domains. In this paper we describe a generic framework that supports the many-to-many connection of formal development environments and theorem provers. Before developing the framework we completed three case studies in order to reveal the main translation issues that need to be addressed. These translation issues were used as input to the requirements for our translation framework. We describe one of these case studies in detail in this paper. We then describe the framework and an Intermediate Modelling Language (IML), which is used to connect the FDEs to the theorem provers. The framework is supported by a collection of translators, both from FDEs (B and CARE) to the IML, and from the IML to theorem provers (Isabelle/HOL, Ergo and Otter). 1
Cite as: Hemer, D., Long, G. and Strooper, P. (2005). Plug-in Proof Support for Formal Development Environments. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 69-79.
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS
 

 

ACS Logo© Copyright Australian Computer Society Inc. 2001-2014.
Comments should be sent to the webmaster at crpit@scem.uws.edu.au.
This page last updated 16 Nov 2007