Мониторинг и тестирование на основе многоуровневых спецификаций программ

В исследованиях по формальным методам разработки и верификации программ много внимания уделяется вопросам построения многоуровневых спецификаций, отвечающих потребностям методологии пошаговой детализации и итеративной разработки. При верификации программ или их моделей наличие нескольких уровней спецификаций также упрощает доказательство свойств, поскольку, как правило, при добавлении нового уточняющего уровня удается переиспользовать те доказательства, которые были выполнены для более абстрактных уровней модели. При тестировании на основе формальных моделей и при мониторинге систем с целью проверки соответствия поведения системы требованиям, заданными формальной моделью, желательно пользоваться теми же моделями, которые использовались при формальной верификации. На практике такие модели в крупных программных системах являются многоуровневыми, однако опыта их использования как основы тестирования и мониторинга пока не было. В статье рассматриваются различные методы построения многоуровневых моделей, новые возможности, которые удается извлечь за счет комбинации функциональных спецификаций и спецификаций архитектуры реализации, ограничения, которые приходится учитывать при организации тестирования и мониторинга на основе многоуровневых моделей.

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.