Deriving specifications of dependable systems

Mazzara M.
 pdf (633K)

Although human skills are heavily involved in the Requirements Engineering process, in particular, in requirements elicitation, analysis and specification, still methodology and formalism play a determining role in providing clarity and enabling analysis. In this paper, we propose a method for deriving formal specifications, which are applicable to dependable software systems. First, we clarify what the method itself is. Computer science has a proliferation of languages and methods, but the difference between the two is not always clear. This is a conceptual contribution. Furthermore, we propose the idea of Layered Fault Tolerant Specification (LFTS). The principle consists in layering specifications in (at least) two different layers: one for normal behaviors and others (if more than one) for abnormal behaviors. Abnormal behaviors are described in terms of an Error Injector (EI), which represent a model of the expected erroneous interference coming from the environment. This structure has been inspired by the notion of an idealized Fault Tolerant component, but the combination of LFTS and EI using rely guarantee thinking to describe interference is our second contribution. The overall result is the definition of a method for the specification of systems that do not run in isolation but in the real, physical world. We propose an approach that is pragmatic to its target audience: techniques must scale and be usable by non-experts, if they are to make it into an industrial setting. This article is making tentative steps, but the recent trends in Software Engineering such as Microservices, smart and software-defined buildings, M2M micropayments and Devops are relevant fields continue the investigation concerning dependability and rely guarantee thinking.

Keywords: formal methods, dependability
Citation in English: Mazzara M. Deriving specifications of dependable systems // Computer Research and Modeling, 2024, vol. 16, no. 7, pp. 1637-1650
Citation in English: Mazzara M. Deriving specifications of dependable systems // Computer Research and Modeling, 2024, vol. 16, no. 7, pp. 1637-1650
DOI: 10.20537/2076-7633-2024-16-7-1637-1650
URL: http://crm-en.ics.org.ru/journal/article/3559/
Creative Commons License This work is licensed under a Creative Commons Attribution-NoDerivs 3.0 Unported License.

Indexed in Scopus

Full-text version of the journal is also available on the web site of the scientific electronic library eLIBRARY.RU

The journal is included in the Russian Science Citation Index

The journal is included in the RSCI

International Interdisciplinary Conference "Mathematics. Computing. Education"

Copyright © 2009–2025 Institute of Computer Science