A Survey of Formal Methods in Software Development

Dines Bjørner (Invited author)

    Research output: Chapter in Book/Report/Conference proceedingConference abstract in proceedingsResearchpeer-review

    Abstract

    The use of formal methods and formal techniques in industry is steadily growing. In this survey we shall characterise what we mean by software development and by a formal method; briefly overview a history of formal specification languages - some of which are: VDM (Vienna Development Method, 1974-..., [1]), Z (Z for Zermelo Fraenkel, 1980-..., [2]), RAISE (Rigorous Approach to Industrial Software Engineering, 1987-..., [3]) Event B (B for Bourbaki, 1990/2000-..., [4]) and Alloy [5]; and outline the basics of a formal development using, for example, RAISE: first developing a domain description D, then a requirements prescription R, and finally a software design S - showing (arguing or formally proving) that S, in the context of D satisfies (is correct with respect to) R. We shall then mention industries in Japan, Europe and USA which, in a number of projects, use formal methods; discuss what it takes for an industry to do so; discuss what education that candidates for these industries need, that is, which courses must be part of a BSc/MSc Software Engineering curriculum. Finally we shall comment on distinctions between formal methods and formal techniques; limitations of mono-language formalisations, hence need for multi-language formalisation (Petri Nets, MSC, StateChart, Temporal Logics); the sociology of university and industry acceptance of formal methods; the inevitability of the use of formal software development methods; while referring to seminal monographs and textbooks on formal methods.
    Original languageEnglish
    Title of host publication2012 19th Asia-Pacific Software Engineering Conference (APSEC)
    Number of pages1
    Volume2
    PublisherIEEE
    Publication date2012
    ISBN (Print)978-1-4673-4930-7
    DOIs
    Publication statusPublished - 2012
    Event19th Asia-Pacific Software Engineering Conference (APSEC 2012) - , Hong Kong
    Duration: 4 Dec 20127 Dec 2012
    http://apsec2012.comp.polyu.edu.hk/

    Conference

    Conference19th Asia-Pacific Software Engineering Conference (APSEC 2012)
    CountryHong Kong
    Period04/12/201207/12/2012
    Internet address
    SeriesAsia Pacific Software Engineering Conference. Proceedings
    ISSN1530-1362

    Bibliographical note

    Keynote Address.

    Fingerprint Dive into the research topics of 'A Survey of Formal Methods in Software Development'. Together they form a unique fingerprint.

    Cite this