OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Extended real-time LOTOS for preemptive systems verification

Sadani, Tarek and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Extended real-time LOTOS for preemptive systems verification. (2007) In: RTNS'07 - 15th International Conference on Real-Time and Network Systems, 29-30 Mars 2007, Nancy, France .

[img](Document in English)

PDF ( Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
261Kb

Official URL: http://rtns07.irisa.fr/

Abstract

Real-time systems not only interact with their environment and hopefully deliver their expected outputs on time. Unlike transformational systems, they may be interrupted at any time while keeping the capacity to restart later on without loosing their state information. Therefore, a real-time system specification language should include a suspend /resume capability. In this paper, we propose to extend the timed process algebra RT-LOTOS with a suspend/resume operator. Extended RT-LOTOS specifications are translated to Stopwatch Time Petri nets that may be analyzed using the TINA tool. We define an RTLOTOS to SwTPN translation pattern. A formal proof is included. Case studies show the interest of our proposal for preemptive systems specification and verification.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE
French research institutions > Centre National de la Recherche Scientifique - CNRS
Laboratory name:
Statistics:download
Deposited By:Pierre de Saqui-Sannes

Repository Staff Only: item control page