Monitoring and Testing Based on Multi-Level Program Specifications
Alexander Konstantinovich PETRENKO,
Denis Valentinovich EFREMOV,
Eugeny Valerievich KORNYKHIN,
Victor Vyacheslavovich KULIAMIN,
Alexey Vladimirovich KHOROSHILOV,
Ilya Viktorovich SHCHEPETKOV https://doi.org/10.15514/ISPRAS-2020-32(6)-1
Abstract
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.
Supporting agencies: This work was supported by the RFBR grant No. 20-01-00568.
About the Authors
Alexander Konstantinovich PETRENKO
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University, Higher School of Economics
Russian Federation
Doctor of Physical and Mathematical Sciences, Professor, Head of the Department of ISP RAS, Professor of Moscow State University and Higher School of Economics
Russian Federation
Doctor of Physical and Mathematical Sciences, Professor, Head of the Department of ISP RAS, Professor of Moscow State University and Higher School of Economics
Denis Valentinovich EFREMOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Junior Researcher
Russian Federation
Junior Researcher
Eugeny Valerievich KORNYKHIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University
Russian Federation
Ph.D. in Physics and Mathematics, leading researcher at ISP RAS, associate professor of system programming departments at Moscow State University and the Higher School of Economics
Russian Federation
Ph.D. in Physics and Mathematics, leading researcher at ISP RAS, associate professor of system programming departments at Moscow State University and the Higher School of Economics
Victor Vyacheslavovich KULIAMIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University, Higher School of Economics
Russian Federation
Ph.D. in Physics and Mathematics, leading researcher at ISP RAS, associate professor of system programming departments at Moscow State University and the Higher School of Economics. Fields of Interest: formal deductive model verification, model-based testing
Russian Federation
Ph.D. in Physics and Mathematics, leading researcher at ISP RAS, associate professor of system programming departments at Moscow State University and the Higher School of Economics. Fields of Interest: formal deductive model verification, model-based testing
Alexey Vladimirovich KHOROSHILOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University, Higher School of Economics, Moscow Institute of Physics and Technology (MIPT)
Russian Federation
Russian Federation
Ilya Viktorovich SHCHEPETKOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. I. Burdonov, A. Kossatchev, A.K. Petrenko, D. Galter. Kvest: Automated generation of test suites from formal specifications. Lecture Notes in Computer Science, vol. 1708, 1999, pp. 608-621.
2. I.B. Bourdonov, A.S. Kossatchev, V.V. Kuliamin, A.K. Petrenko. UniTesK test suite architecture, Lecture Notes in Computer Science, vol. 2391, 2002, pp. 77-88.
3. SpecExporer. URL: https://docs.microsoft.com/ru-ru/archive/msdn-magazine/2013/december/model-based-testing-an-introduction-to-model-based-testing-and-spec-explorer, accessed 21.12.2020.
4. JML (Java Modeling Language), URL: http://www.eecs.ucf.edu/~leavens/JML//index.shtml, accessed 21.12.2020.
5. M. Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. Lecture Notes in Computer Science, vol. 3362, 2004, pp. 49-69.
6. ACSL (ANCI/ISO C Specification Language). https://www.academia.edu/16532644/ACSL_ANSI_ISO_C_Specification_Language, accessed 21.12.2020.
7. SPARK. http://www.spark-2014.org, accessed 21.12.2020.
8. П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Моделирование и верификация политик безопасности управления доступом в операционных системах. М., Горячая линия – Телеком, 2019 г., 214 стр. / P.N. Devyanin, D.V. Efremov, V.V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Modeling and verification of access control security policies in operating systems. M., Hotline – Telecom, 2019, 214 p. (in Russian).
9. Y. Gurevich. Evolving algebras 1993: Lipari guide. In: Börger E. (ed.) Specification and Validation Methods, pp. 9-36. Oxford University Press, Oxford, 1995.
10. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 2005, 815 p.
11. J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010, 612 p.
12. L. Lamport. Specifying Concurrent Systems with TLA+. In: Broy M., Steinbrüggen R. (eds). Calculational System Design, pp. 183–247. IOS Press, Amsterdam, 2000.
13. D. Bjorner, C.B. Jones. The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol. 61, 1978.
14. J.-R. Abrial. Data Semantics. In Proc. of the IFIP Working Conference on Data Base Management, 1974, pp. 1–59.
15. C.B. Nielsen, P.G. Larsen, J. Fitzgerald, J. Woodcock. Systems of systems engineering: basic concepts, model-based techniques, and research directions. ACM Computing Surveys (CSUR), vol. 48, issue 4, 2015, article no. 18.
16. C. Danmin, S. Yue, C. Zhiguo. A Formal Specification in B of an Operating System. The Open Cybernetics & Systemics Journal, no. 9, 2015, pp. 1124-1129.
17. L. Ren, R. Chang, Q. Yin, W. Wang. Using the B Method to Formalize Access Control Mechanism with TrustZone Hardware Isolation. Lecture Notes in Computer Science, vol. 10701, 2017, pp. 759-769.
18. S. Hallerstede. M. Hasangic, S. Krings, P.G. Larsen, M. Leuschel. From Software Specifications to Constraint Programming. Lecture Notes in Computer Science, vol. 10886, 2018, pp. 21-36.
19. D. Efremov, I. Shchepetkov. Runtime Verification of Linux Kernel Security Module. Lecture Notes in Computer Science, vol. 12233, 2020, pp. 185-199.
20. V. Kuliamin, A. Khoroshilov, D. Medvedev. Formal Modeling of Multi-Level Security and Integrity Control Implemented with SELinux. In Proc. of the 2019 Actual Problems of Systems and Software Engineering (APSSE), 2019, pp. 131-136.
Review
For citations:
PETRENKO A.K., EFREMOV D.V., KORNYKHIN E.V., KULIAMIN V.V., KHOROSHILOV A.V., SHCHEPETKOV I.V. Monitoring and Testing Based on Multi-Level Program Specifications. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):7-18. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-1
Email this article 