Proof support for RAISE - by a Reuse Approach Based on Institutions

Formal methods are mathematically based methods for developing software. Such methods usually involve that software and requirements are specified in a formal specification language, after which it is verified that the software meets the requirements. RAISE is a formal method with the associated specification language RSL and a proof system. Computer-based proof tools are available for RAISE, but a higher degree of automation is desired. Isabelle/HOL is a proof assistant for higher-order logic (HOL). It is an instantiation of the generic proof assistant Isabelle which offers a suitable degree of automation and flexibility. In order to use the Isabelle/HOL proof assistant for the RAISE method, translation from RSL to HOL is considered. The translation is based on institutions which formalize the informal notion of "a logical system". Institutions and morphisms between institutions are presented together with specifications over institutions and model-theoretic semantics of specifications. The concept of "light institution comorphisms" is introduced as a modification of well-known institution comorphisms, and it is proved that a light institution comorphism enables sound reuse of proof assistants when it has certain properties. Moreover, the concept of looser semantics of specifications is introduced as a model-theoretic description of the semantics of RSL specifications, and an equivalence result is proved. An institution for an applicative, deterministic subset of RSL, referred to as "mRSL", is defined. Then, a well-known institution for HOL is presented, and Isabelle/HOL is briefly described. An institution comorphism from the mRSL institution to the HOL institution is defined, providing a translation from mRSL to Isabelle/HOL, and it is proved that the light institution comorphism has the properties that enable sound reuse of the Isabelle/HOL proof assistant. The use of the translation is described in connection with three examples: logical circuits, a generalized railway crossing, and an encoding of Duration Calculus in RSL. In Danish: Formelle metoder er matematisk baserede metoder til udvikling af programmel. Sådanne metoder involverer som regel, at programmel og krav beskrives i et formelt specifikationssprog, hvorefter det verificeres, at programmellet opfylder de ønskede krav. RAISE er en formel metode med det tilhørende specifikationssprog RSL og et bevissystem. Der findes datamatbaserede bevisværktøjer til RAISE, men en højere grad af automation er ønskværdig. Isabelle/HOL er en bevisfører for højereordens logik (HOL). Bevisføreren er en instantiering af den generiske bevisfører Isabelle, der tilbyder en passende grad af automation og fleksibilitet. Med henblik på at benytte bevisføreren Isabelle/HOL i forbindelse med RAISE metoden, betragtes oversættelse fra RSL til HOL. Oversættelsen baseres på institutioner, der formaliserer det uformelle begreb "logisk system ". Institutioner og morfier mellem institutioner gennemgås sammen med specifikationer over institutioner og modelteoretisk semantik af specifikationer. Begrebet "let institutionscomorfi" introduceres som en modifikation af velkendte institutionscomorfier, og det bevises, at en let institutionscomorfi muliggør sund genbrug af bevisførere, når den har visse egenskaber. Derudover introduceres begrebet løsere semantik af specifikationer som en modelteoretisk beskrivelse af semantikken af RSL- specifikationer, og et ækvivalensresultat bevises. Der defineres en institution for en applikativ, deterministisk delmængde af RSL, der benævnes "mRSL". Herefter præsenteres en velkendt institution for HOL, og Isabelle/HOL gennemgås kort. Der defineres en let institutionscomorfi fra mRSL- institutionen til HOL-institutionen, hvorved der fås en oversættelse fra mRSL til Isabelle/HOL, og det bevises, at den definerede lette institutionscomorfi har de egenskaber, der muliggør sund genbrug af bevisføreren Isabelle/HOL. Brugen af den definerede oversættelse beskrives i forbindelse med tre eksempler: logiske kredsløb, en jernbaneoverskæring og en indkodning af varighedskalkylen i RSL.