Open AccessMonitoring and Testing Based on Multi-Level Program Specifications
Author(s) -
Александр Константинович Петренко,
Denis Efremov,
Евгений Валерьевич Корныхин,
Виктор Вячеславович Кулямин,
А. В. Хорошилов,
Илья Викторович Щепетков
Publication year - 2020
Publication title -
trudy instituta sistemnogo programmirovaniâ ran/trudy instituta sistemnogo programmirovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2220-6426
pISSN - 2079-8156
DOI - 10.15514/ispras-2020-32(6)-1
Subject(s) - computer science , reuse , conformance testing , formal methods , mathematical proof , software engineering , verification and validation , formal specification , set (abstract data type) , formal verification , reliability engineering , programming language , engineering , geometry , mathematics , waste management , standardization , operating system , operations management
Research on formal methods of software development and verification focuses on building specifications using incremental and iterative development methodologies. The presence of several levels of specifications simplifies proving of properties, since it is possible to reuse the proofs that were performed for more abstract layers of the model. It is desirable to use the same models that were used for formal verification also in testing of real systems for compliance with the requirements set by these models. In practice, large software systems are described by multi-level models. There was no experience of using such models as the basis for testing and monitoring. The paper discusses various methods for developing multi-level models, new opportunities that can be obtained through a combination of functional specifications and implementation-level refinements, limitations that must be considered during testing and monitoring of real systems for compliance with multi-level models.