Model Integration for Formal Qualification of Timing-Aware Software Data Acquisition Components 1
Computers are increasingly used for process control systems (transport systems, industrial processes). The role of these computers is to implement control laws using data (giving information about the process state) coming from sensors and producing outputs (command) to control a process using actuators. Due to the dynamic evolution of the controlled process, a control law implementation needs to satisfy some timing constraints (data arrival law, data lost rate, time interval between data update and command production) [WIT 95], [SWT 05], [TOR 98], [FEN 01]. Because most of these systems are critical systems, timing constraints are to be a priori (before execution) formally validated.
Critical constraints lead to predictable systems that induce hand-made and code-centric developments. Nowadays, these systems are increasingly complex and reuse of software components will both help the designer and reduce development cost. In this domain, because of critical timing constraints, reusable components must be timing-aware components.
In the process control domain, reusable software components are classically execution services provided by a Real-Time Operating System respecting standards such as OSEK [OSEK] or POSIX [POSIX] remote communication services (FT layer of TTA [SCH 97]) and device drivers. In this work, we consider sensor drivers, that is to say the ...