An Ontology of Specification Patterns for Verification of Concurrent Systems
Natalia Olegovna Garanina, Vladimir Zubin, Tatiana Lyakh, Sergei Petrovich Gorlatch · Frontiers in artificial intelligence and applications · 2018
Verifying the reliability of software systems formally is difficult due to the complexity of system correctness requirements. Specification patterns allow us to describe typical requirements in a natural language, while their formal semantics enable expressing these requirements in the input language of some verification tool. In this paper, we propose an ontology of specification patterns that combines patterns from existing requirement classifications with new patterns. Our ontology can be used to express combinations of requirements of the following types: qualitative, real and branching time, with combined events, quantitative characteristics of events, and simple statements about data. The advantage of our approach is the ability to formally verify the compatibility of multiple requirements. As an illustrating use case, we describe the requirements for the real-world vacuum control system of the Large Solar Vacuum Telescope.