A contract-based method to specify stimulus-response requirements

The verification of many practical systems - in particular, embedded systems - involves processes executing over time, for which it is common to use models based on temporal logic, in either its linear (LTL) or branching (CTL). Some of today’s most advanced automatic program verifiers, however, rely...

Full description

Bibliographic Details

Published in:	Труды Института системного программирования РАН
Main Authors:	A. Naumchev, M. Mazzara, B. Meyer, J.-M. Bruel, F. Galinier, S. Ebersold
Format:	Article
Language:	English
Published:	Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
Subjects:	бесшовные требования проектирование по контракту autoproof эйфель система контроля шасси
Online Access:	https://ispranproceedings.elpub.ru/jour/article/view/312