ON THE FORMAL SPECIFICATION AND VERIFICATION OF AUTOMATA-BASED PROGRAMS BY SPECIFICATION PATTERNS

Клебанов А.А., A. A. Shalyto


Read the full article  ';

Abstract

Model checking is a well developed verification technique; still it is not widely adopted. One of the reasons is that defining formal specification as a set of temporal logic formulae is an error-prone and time-consuming task. This paper gives an overview of the research which focuses on expressing verifiable requirements in a controlled natural language in the framework of automata-based programming. Applicability of the specification patterns in scope of automata-based approach is investigated. Also a formal grammar is introduced to derivate the requirements.


Keywords: automata-based programming, model checking, temporal logic

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика