@PHDTHESIS\{IMM2004-03148,
    author       = "M. P. Lindegaard",
    title        = "Proof support for {RAISE} -  by a Reuse Approach Based on Institutions",
    year         = "2004",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Assoc. Prof.  Anne E. Haxthausen  and Assoc. Prof.  Michael R. Hansen",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3148-full.html",
    abstract     = "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{\aa}danne metoder involverer som regel, at programmel og krav beskrives i et formelt specifikationssprog, hvorefter det verificeres, at programmellet opfylder de {\o}nskede krav.

{RAISE} er en formel metode med det tilh{\o}rende specifikationssprog {RSL} og et bevissystem. Der findes datamatbaserede bevisv{\ae}rkt{\o}jer til {RAISE,} men en h{\o}jere grad af automation er {\o}nskv{\ae}rdig.

Isabelle/{HOL} er en bevisf{\o}rer for h{\o}jereordens logik (HOL). Bevisf{\o}reren er en instantiering af den generiske bevisf{\o}rer Isabelle, der tilbyder en passende grad af automation og fleksibilitet. 

Med henblik p{\aa} at benytte bevisf{\o}reren Isabelle/{HOL} i forbindelse med {RAISE} metoden, betragtes overs{\ae}ttelse fra {RSL} til {HOL}. Overs{\ae}ttelsen baseres p{\aa} institutioner, der formaliserer det uformelle begreb {''}logisk system ''.

Institutioner og morfier mellem institutioner gennemg{\aa}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{\o}r sund genbrug af bevisf{\o}rere, n{\aa}r den har visse egenskaber. Derudover introduceres begrebet  l{\o}sere semantik af specifikationer  som en modelteoretisk beskrivelse af semantikken af {RSL-} specifikationer, og et {\ae}kvivalensresultat bevises.

Der defineres en institution for en applikativ, deterministisk delm{\ae}ngde af {RSL,} der ben{\ae}vnes {''}mRSL''. Herefter pr{\ae}senteres en velkendt institution for {HOL,} og Isabelle/{HOL} gennemg{\aa}s kort. Der defineres en let institutionscomorfi fra mRSL- institutionen til {HOL-}institutionen, hvorved der f{\aa}s en overs{\ae}ttelse fra mRSL til Isabelle/{HOL,} og det bevises, at den definerede lette institutionscomorfi har de egenskaber, der muligg{\o}r sund genbrug af bevisf{\o}reren Isabelle/HOL. 

Brugen af den definerede overs{\ae}ttelse beskrives i forbindelse med tre eksempler: logiske kredsl{\o}b, en jernbaneoversk{\ae}ring og en indkodning af varighedskalkylen i {RSL}."
}