A formal framework for verifying distributed embedded systems based on abstraction methods |
| |
Authors: | Francois Carcenac Frederic Boniol |
| |
Affiliation: | (1) ONERA-CERT, Toulouse, France |
| |
Abstract: | This paper presents a formal framework for verifying distributed embedded systems. An embedded system is described as a set of concurrent real time functions which communicate through a network of interconnected switches involving messages queues and routing services.In order to allow requirements verification, such a model is then translated into timed automata. However, the complexity inherent in distributed embedded systems often does not allow to apply model checking techniques. Consequently, the paper presents an abstraction-based verification method which consists in abstracting the communication network by end-to-end timed channels. To prove a given safety property φ requires then (1) to prove a set of proof obligations ensuring the correctness of the abstraction step (i.e. the end-to-end channels correctly abstract the network), and (2) to prove φ at the abstract level. The expected advantage of such a method lies in the ability to overcome the combinatorial explosion frequently met when verifying complex systems. This method is illustrated by an avionic case study. |
| |
Keywords: | Distributed embedded systems Timed automata Model checking Abstraction Compositional verification |
本文献已被 SpringerLink 等数据库收录! |