Formality in requirements: new publication
The best way to make software requirements precise is to use one of the available “formal” approaches. Many have been proposed; I am not aware of a general survey published so far. Over the past two years, we have been working on a comprehensive survey of the use of formality in requirements, of which we are now releasing a draft. “We” is a joint informal research group from Innopolis University and the University of Toulouse, whose members have been cooperating on requirements issues, resulting in publications listed under “References” below and in several scientific events.
The survey is still being revised, in particular because it is longer than the page limit of its intended venue (ACM Computing Surveys), and some sections are in need of improvement. We think, however, that the current draft can already provide a solid reference in this fundamental area of software engineering.
The paper covers a broad selection of methods, altogether 22 of them, all the way from completely informal to strictly formal. They are grouped into five categories: natural language, semi-formal, automata- or graph-based, other mathematical frameworks, programming-language based. Examples include SysML, Relax, Statecharts, VDM, Eiffel (as a requirements notation), Event-B, Alloy. For every method, the text proposes a version of a running example (the Landing Gear System, already used in some of our previous publications) expressed in the corresponding notation. It evaluates the methods using a set of carefully defined criteria.
The paper is: Jean-Michel Bruel, Sophie Ébersold, Florian Galinier, Alexandr Naumchev, Manuel Mazzara and Bertrand Meyer: Formality in Software Requirements, draft, November 2019.
The text is available here. Comments on the draft are welcome.
References
Bertrand Meyer, Jean-Michel Bruel, Sophie Ebersold, Florian Galinier and Alexandr Naumchev: Towards an Anatomy of Software Requirements, in TOOLS 2019, pages 10-40, see here (or arXiv version here). I will write a separate blog article about this publication.
Alexandr Naumchev and Bertrand Meyer: Seamless requirements. Computer Languages, Systems & Structures 49, 2017, pages 119-132, available here.
Florian Galinier, Jean-Michel Bruel, Sophie Ebersold and Bertrand Meyer: Seamless Integration of Multirequirements, in Complex Systems, 25th International Requirements Engineering Conference Workshop, IEEE, pages 21-25, 2017, available here.
Alexandr Naumchev, Manuel Mazzara, Bertrand Meyer, Jean-Michel Bruel, Florian Galinier and Sophie Ebersold: A contract-based method to specify stimulus-response requirements, Proceedings of the Institute for System Programming, vol. 29, issue 4, 2017, pp. 39-54. DOI: 10.15514, available here.
Alexandr Naumchev and Bertrand Meyer: Complete Contracts through Specification Drivers., in 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 160-167, 2016, available here.
Alexandr Naumchev, Bertrand Meyer and Víctor Rivera: Unifying Requirements and Code: An Example, in PSI 2015 (Ershov conference, Perspective of System Informatics), pages 233-244, available here.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy
Business Object Notation wasn’t mentioned. Do you believe SysML subsumes this?
Dear Bertrand and dear Co-authors,
thanks a lot for the interesting paper.
Connecting to the current ideas, those highlighted below from the following publication may be further fertilizing:
– Biró M., Kossak F., Klespitz J., Kovács L. (2017) Graceful Integration of Process Capability Improvement, Formal Modeling and Web Technology for Traceability. In: Stolfa J., Stolfa S., O’Connor R., Messnarz R. (eds) Systems, Software and Services Process Improvement. Communications in Computer and Information Science, vol 748. pp 381-398. Springer, Cham. URL http://dx.doi.org/10.1007/978-3-319-64218-5_32
Full text preprint available at:
https://www.researchgate.net/publication/319061671_Graceful_Integration_of_Process_Capability_Improvement_Formal_Modeling_and_Web_Technology_for_Traceability
Brief highlights:
Formal modeling is fundamentally necessary for securing completeness and consistency, but customarily rejected due to the usually prohibiting up-front effort needed to formally process all artifacts of an already established traditional system; Graceful integration can considerably lower this threshold.
One of the features of the new approach, of high importance for actual applications but rarely considered by promoters of formal modeling, is that it is possible to introduce the newly designed requirements management system incrementally, so that only new or changed requirements are affected and traced. This means that only new or changed requirements need to be formally modeled at the start, making the operational introduction of the new system practically feasible.
The term “graceful integration” is used for the above capability of incrementally introducing formal modeling.
In contrast to the established term “graceful degradation” for the ability of a system to maintain functionality when portions of the system break down, “graceful integration” means the ability of a system to be incremented so that its functionality is improved without significant disruption.
For consistency checking however, a formalized representation of all relevant requirements will have to be available.
The need for the feature of the incremental introduction of the formal modeling based system originates from actual safety-critical software development for active medical devices (Hemodialysis Safety System) providing the fundamental industrial background of the research similarly to the “Landing Gear System” used in your research.
As a further link between our ideas, one of the key co-authors (Felix Kossak) of the above “Graceful Integration…” paper also contributed an ASM-based solution to the same Landing Gear System Case Study you use as industrial background :-)
https://link.springer.com/chapter/10.1007/978-3-319-07512-9_10
I wish you all the best,
Miklos