Kronos
KRONOS is a tool developed with the aim to verify complex real-time systems. Real-time systems are systems that must perform a task within strict time deadlines. Embedded controllers, circuits and communication protocols are examples of such time-dependent systems. These systems are often part of complex safety-critical applications such as aircraft avionics, which are very difficult to design and analyze, but whose correct behavior must be ensured because failures may have severe consequences. Hence, real-time systems need to be rigorously modeled and specified in order to be able to formally prove their correctness with respect to the desired requirements. In KRONOS, components of real-time systems are modeled by timed automata and the correctness requirements are expressed in the real-time temporal logic TCTL.
Keywords for this software
References in zbMATH (referenced in 226 articles , 1 standard article )
Showing results 1 to 20 of 226.
Sorted by year (- Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
- Benerecetti, Massimo; Peron, Adriano: Timed recursive state machines: expressiveness and complexity (2016)
- Camacho, Carlos; Llana, Luis; Núñez, Alberto: Cost-related interface for software product lines (2016)
- Bouyer, Patricia; Markey, Nicolas; Sankur, Ocan: Robust reachability in timed automata and games: a game-based approach (2015)
- Motallebi, Hassan; Azgomi, Mohammad Abdollahi: Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques (2015)
- Volkanov, D.Yu.; Zakharov, V.A.; Zorin, D.A.; Podymov, V.V.; Konnov, I.V.: A combined toolset for the verification of real-time distributed systems (2015)
- Andrychowicz, Marcin; Dziembowski, Stefan; Malinowski, Daniel; Mazurek, Łukasz: Modeling bitcoin contracts by timed automata (2014)
- Byg, Joakim; Jacobsen, Morten; Jacobsen, Lasse; Jørgensen, Kenneth Yrke; Møller, Mikael Harkjær; Srba, Jiří: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata (2014)
- David, Alexandre; Fang, Huixing; Larsen, Kim Guldstrand; Zhang, Zhengkui: Verification and performance evaluation of timed game strategies (2014)
- Geeraerts, Gilles; Raskin, Jean-François; Sznajder, Nathalie: On regions and zones for event-clock automata (2014)
- Konur, Savas; Fisher, Michael; Dobson, Simon; Knox, Stephen: Formal verification of a pervasive messaging system (2014)
- Lampka, Kai; Giannopoulou, Georgia; Pellizzoni, Rodolfo; Wu, Zheng; Stoimenov, Nikolay: A formal approach to the WCRT analysis of multicore systems with memory contention under phase-structured task sets (2014)
- Moser, Heinrich; Schmid, Ulrich: Reconciling fault-tolerant distributed algorithms and real-time computing (2014)
- Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2014)
- Sankur, Ocan; Bouyer, Patricia; Markey, Nicolas: Shrinking timed automata (2014)
- Balaguer, Sandie; Chatain, Thomas: Avoiding shared clocks in networks of timed automata (2013)
- Gómez, Rodolfo: Model-checking timed automata with deadlines with Uppaal (2013)
- Hiraishi, Kunihiko; Kobayashi, Koich: An approximation algorithm for box abstraction of transition systems on real state spaces (2013)
- Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: A timed CTL model checker for real-time maude (2013)
- Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)