TAXYS: A tool for the development and verification of real-time embedded systems The correct behavior of real-time applications depends not only on the correctness of the results of computations but also on the times at which these results are produced. As a matter of fact, violations of real-time constraints in embedded systems are the most difficult errors to detect, because they are extremely sensitive both to the patterns of external events stimulating the system and to the timing behavior of the system itself. Clearly, the development of real-time systems requires rigorous methods and tools to reduce development costs and “time-to-market” while guaranteeing the quality of the produced code (in particular, respect of the temporal constraints). The above requirements motivated the development of the TAXYS tool, dedicated to the design and validation of real-time telecommunications software. One of the major goal of the TAXYS tool is to produce a formal model that captures the temporal behavior of the whole application which is composed of the embedded computer and its external environment. For this purpose we use the formal model of timed automata. The choice of this model allows the use of results, algorithms and tools available. Here, we use the KRONOS model checker for model analysis. From the source code of the application, an ESTEREL program annotated with temporal constraints, the TAXYS tool produces on the one hand a sequential executable code and on the other hand a timed model of the application. This model is again composed with a timed model of the external environment in order to obtain a global model which is statically analyzed to validate timing constraints. This validation should notably shorten design time by limiting tedious test and simulation sessions

References in zbMATH (referenced in 20 articles , 1 standard article )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  2. Ghosal, Arkadeb; Iercan, Daniel; Kirsch, Christoph M.; Henzinger, Thomas A.; Sangiovanni-Vincentelli, Alberto: Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code (2012) ioport
  3. Ju, Lei; Huynh, Bach Khoa; Roychoudhury, Abhik; Chakraborty, Samarjit: Performance debugging of Esterel specifications (2012) ioport
  4. Bauer, Kerstin; Schneider, Klaus: From synchronous programs to symbolic representations of hybrid systems (2010)
  5. Bucci, Giacomo; Carnevali, Laura; Ridi, Lorenzo; Vicario, Enrico: Oris: a tool for modeling, verification and evaluation of real-time systems (2010) ioport
  6. de Boer, Frank; Chothia, Tom; Jaghoori, Mohammad Mahdi: Modular schedulability analysis of concurrent objects in Creol (2010)
  7. de Boer, Frank S.; Jaghoori, Mohammad Mahdi; Johnsen, Einar Broch: Dating concurrent objects: Real-time modeling and schedulability analysis (2010) ioport
  8. Jaghoori, Mohammad Mahdi; de Boer, Frank S.; Chothia, Tom; Sirjani, Marjan: Schedulability of asynchronous real-time concurrent objects (2009)
  9. Bianco, Vieri del; Lavazza, Luigi; Mauri, Marco; Occorso, Giuseppe: Towards uML-based formal specifications of component-based real-time software (2007) ioport
  10. Carloni, Luca P.; Passerone, Roberto; Pinto, Alessandro; Sangiovanni-Vincentelli, Alberto L.: Languages and tools for hybrid systems design. (2006)
  11. Poddar, Rajiv Kumar; Bhaduri, Purandar: Verification of Giotto based embedded control systems (2006)
  12. Tripakis, Stavros; Yovine, Sergio; Bouajjani, Ahmed: Checking timed Büchi automata emptiness efficiently (2005)
  13. Ghosal, Arkadeb; Henzinger, Thomas A.; Kirsch, Christoph M.; Sanvido, Marco A.A.: Event-driven programming with logical execution times (2004)
  14. Del Bianco, Vieri; Lavazza, Luigi; Mauri, Marco; Occorso, Giuseppe: Towards UML-based formal specifications of component-based real-time software (2003)
  15. Graf, Susanne: Expression of time and duration constraints in SDL (2003)
  16. Dillenseger, Bruno; Tagant, Anne-Marie; Hazard, Laurent: Programming and executing telecommunication service logic with Moorea reactive mobile agents (2002)
  17. Koo, T.John; Liebman, Judith; Ma, Cedric; Horowitz, Benjamin; Sangiovanni-Vincentelli, Alberto; Sastry, Shankar: Platform-based embedded software design for multi-vehicle multi-modal systems (2002)
  18. Sifakis, Joseph: Scheduler modeling based on the controller synthesis paradigm (2002) ioport
  19. Closse, Etienne; Poize, Michel; Pulou, Jacques; Sifakis, Joseph; Venter, Patrick: TAXYS: A tool for the development and verification of real-time embedded systems (2001)
  20. Sifakis, Joseph: Modeling real-time systems -- challenges and work directions (2001)