Using formal models to cross check an implementation
In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing System EICS 2016. pages 126-137. 2016.
Raquel Oliveira, Sophie Dupuy-Chessa, Gaëlle Calvary, Danièle Dadolle
Abstract
Interactive systems are developed according to requirements, which may be, for instance, documentation, prototypes, diagrams, etc. The informal nature of system requirements may be a source of problems: it may be the case that a system does not implement the requirements as expected, thus, a way to validate whether an implementation follows the requirements is needed. We propose a novel approach to validating a system using formal models of the system. In this approach, a set of traces generated from the execution of the real interactive system is searched over the state space of the formal model. The scalability of the approach is demonstrated by an application to an industrial system in the nuclear plant domain. The combination of trace analysis and formal methods provides feedback that can bring improvements to both the real interactive system and the formal model.