SAS architecture: verification oriented formal modeling of concrete critical systems

Concrete critical systems validation is a major challenge in any development process. Model checking verification offers exhaustive and automated validation. To apply this methodology, the specification of critical systems must be supported by a formal mathematical well-sounded model. To this end, we rely on synchronous language to model such systems and to ensure model existence we consider systems falling into a particular SAS architecture. SAS systems are composed by a synchronous main controller that manages autonomic asynchronous tasks. Abstraction methods provide us with the required synchronous model. We show how our approach suits wearable computer applications designing and how the modeling we propose meets the requirements of wearable computer validation.