%0 Journal Article %1 bjorner00formal %A Bjørner, Dines %D 2000 %J Annals of Software Engineering %K research.cs.softeng info.refs.journals.ansoft research.cs.softeng.formal %N 1 %P 11--66 %T Pinnacles of software engineering: 25 years of formal methods %U http://dx.doi.org/10.1023/A:1018983515535 %V 10 %X Abstract  In this invited paper we review 25 years of propagating formal specification in software engineering. We will do so throughoutlining a paradigmatic approach to the practice of software engineering. For the sake of contrasting argument we shall claimthat this approach stands in sharp contrast to classical engineering – and that there is little help to be obtained from classicalengineering in securing the quality of the most important facets of software engineering! We shall be outlining a softwareengineering* practice in which formal techniques are applied in capturing the application domain void of any reference torequirements let alone software; and in then capturing requirements: Domain requirements (projected, instantiated, possiblyextended and usually initialised from domain descriptions), interface requirements and machine requirements. The softwareengineering practice then goes on to design the software: First the architecture, then the program structure, etc. Throughoutabstraction and modelling, hand�?in�?hand, are used in applicative (functional), imperative and process oriented descriptions,from loose specifications towards concrete, instantiated descriptions, using hierarchical as well as configurational modelling,denotational as well as computational modelling, and in structuring even small scale descriptions using appropriate modularisationconcepts: Schemes, classes and objects. All the concepts spelled in this font are software engineering “program�? descriptionnotions that have been honed over the years, starting in 1973 with VDM Bekić et al. 1974; Bjrner and Jones 1978, 1982band continuing with RAISE Group 1992, 1995. The current status of our approach to software engineering, based on extensive,but not exclusive use of formal techniques, developed significantly during my years as UN Director of the UN University'sInternational Institute for Software Technology (UNU/IIST) in Macau, 1992–1997. Many large scale software developments basedon the domain/requirements/software design paradigm outlined here were systematically applied to the experimental developmentof software designs for the computing support of a number of diverse infrastructure components**. Special boxes, scatteredthroughout the text, highlight ‘pinnacle’ contribution by named computer and computing scientists as well as by specific R&Dprojects.

@article{bjorner00formal, abstract = {Abstract  In this invited paper we review 25 years of propagating formal specification in software engineering. We will do so throughoutlining a paradigmatic approach to the practice of software engineering. For the sake of contrasting argument we shall claimthat this approach stands in sharp contrast to classical engineering – and that there is little help to be obtained from classicalengineering in securing the quality of the most important facets of software engineering! We shall be outlining a softwareengineering* practice in which formal techniques are applied in capturing the application domain void of any reference torequirements let alone software; and in then capturing requirements: Domain requirements (projected, instantiated, possiblyextended and usually initialised from domain descriptions), interface requirements and machine requirements. The softwareengineering practice then goes on to design the software: First the architecture, then the program structure, etc. Throughoutabstraction and modelling, hand�?in�?hand, are used in applicative (functional), imperative and process oriented descriptions,from loose specifications towards concrete, instantiated descriptions, using hierarchical as well as configurational modelling,denotational as well as computational modelling, and in structuring even small scale descriptions using appropriate modularisationconcepts: Schemes, classes and objects. All the concepts spelled in this font are software engineering “program�? descriptionnotions that have been honed over the years, starting in 1973 with VDM [Bekić et al. 1974; Bjrner and Jones 1978, 1982b]and continuing with RAISE [Group 1992, 1995]. The current status of our approach to software engineering, based on extensive,but not exclusive use of formal techniques, developed significantly during my years as UN Director of the UN University'sInternational Institute for Software Technology (UNU/IIST) in Macau, 1992–1997. Many large scale software developments basedon the domain/requirements/software design paradigm outlined here were systematically applied to the experimental developmentof software designs for the computing support of a number of diverse infrastructure components**. Special boxes, scatteredthroughout the text, highlight ‘pinnacle’ contribution by named computer and computing scientists as well as by specific R&Dprojects.}, added-at = {2009-06-25T16:50:52.000+0200}, author = {Bjørner, Dines}, biburl = {https://www.bibsonomy.org/bibtex/2775adc3e72457ec3c9882c4c849fd16a/msn}, description = {SpringerLink - Journal Article}, file = {bjorner00formal.pdf:papers\\ansoft\\bjorner00formal.pdf:PDF}, interhash = {f94db0662d145913d06af83d1c73935a}, intrahash = {775adc3e72457ec3c9882c4c849fd16a}, journal = {Annals of Software Engineering}, keywords = {research.cs.softeng info.refs.journals.ansoft research.cs.softeng.formal}, month = {#nov#}, number = 1, pages = {11--66}, timestamp = {2009-06-25T16:50:52.000+0200}, title = {Pinnacles of software engineering: 25 years of formal methods}, url = {http://dx.doi.org/10.1023/A:1018983515535}, volume = 10, year = 2000 }