Formalisation method for decription of embedded system behavior during software development

Автор: Krasnov N.V., Nebylov A.V., Samokish A.V.

Журнал: Научное приборостроение @nauchnoe-priborostroenie

Рубрика: Обработка и представление данных

Статья в выпуске: 3 т.21, 2011 года.

Бесплатный доступ

This article analyzes the formalization method for embedded system initial data behavior description using temporal formulas and Kripke structure. The formalization process is exemplified by the description of automatic cholinesterase activity level analyzer for human plasma and blood "Granat-4". The obtained formalized description can be used for software development, system analysis with Model Checking, formal verification and preparing test planes.

Formalization, verification, kripke structure, temporal logic, cholinesterase, transition system, use case

Короткий адрес: https://sciup.org/14264730

IDR: 14264730

Статья научная