Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2020-32(6)-1

Полный текст:

Аннотация

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

Об авторах

Александр Константинович ПЕТРЕНКО
Институт системного программирования им. В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики
Россия
Доктор физико-математических наук, профессор, начальник отдела ИСП РАН, профессор МГУ и ВШЭ


Денис Валентинович ЕФРЕМОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Младший научный сотрудник


Евгений Валерьевич КОРНЫХИН
Институт системного программирования им. В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова
Россия
Кандидат физико-математических наук, доцент кафедры системного программирования МГУ, старший научный сотрудник ИСП РАН


Виктор Вячеславович КУЛЯМИН
Институт системного программирования им.В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики
Россия
Кандидат физико-математических наук, ведущий научный сотрудник ИСП РАН, доцент кафедр системного программирования МГУ и ВШЭ


Алексей Владимирович ХОРОШИЛОВ
Институт системного программирования им.В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, НИУ Высшая школа экономики, Московский физико-технический институт
Россия
Кандидат физико-математических наук, ведущий научный сотрудник, директор Центра верификации ОС Linux в ИСП РАН, доцент кафедр системного программирования МГУ, ВШЭ и МФТИ


Илья Викторович ЩЕПЕТКОВ
Институт системного программирования им.В.П. Иванникова РАН
Россия
Стажер-исследователь


Список литературы

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.


Для цитирования:


ПЕТРЕНКО А.К., ЕФРЕМОВ Д.В., КОРНЫХИН Е.В., КУЛЯМИН В.В., ХОРОШИЛОВ А.В., ЩЕПЕТКОВ И.В. Мониторинг и тестирование на основе многоуровневых спецификаций программ. Труды Института системного программирования РАН. 2020;32(6):7-18. https://doi.org/10.15514/ISPRAS-2020-32(6)-1

For citation:


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

Просмотров: 83


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)