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

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


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-SUPAERO (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Laboratory name:
Deposited On:11 Mar 2009 13:51

Repository Staff Only: item control page