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.

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

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

1 2 3 ... 12 13 14 next

  1. Clemente, Lorenzo; Lasota, Sławomir: Reachability relations of timed pushdown automata (2021)
  2. Mari, Thomas; Dang, Thao; Gössler, Gregor: Explaining safety violations in real-time systems (2021)
  3. Baresi, L.; Bersani, M. M.; Marconi, F.; Quattrocchi, G.; Rossi, M.: Using formal verification to evaluate the execution time of Spark applications (2020)
  4. Bartoletti, Massimo; Bocchi, Laura; Murgia, Maurizio: Progress-preserving refinements of CTA (2018)
  5. Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim Guldstrand; Markey, Nicolas; Ouaknine, Joël; Worrell, James: Model checking real-time systems (2018)
  6. Gastin, Paul; Mukherjee, Sayan; Srivathsan, B.: Reachability in timed automata with diagonal constraints (2018)
  7. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  8. Seshia, Sanjit A.; Sharygina, Natasha; Tripakis, Stavros: Modeling for verification (2018)
  9. Wang, Xi; Li, Zhiwu; Wonham, W. M.: Priority-free conditionally-preemptive scheduling of modular sporadic real-time systems (2018)
  10. Zaatiti, Hadi; Ye, Lina; Dague, Philippe; Gallois, Jean-Pierre; Travé-Massuyès, Louise: Abstractions refinement for hybrid systems diagnosability analysis (2018)
  11. Al-Bataineh, Omar; Reynolds, Mark; French, Tim: Finding minimum and maximum termination time of timed automata models with cyclic behaviour (2017)
  12. Lorber, Florian; Rosenmann, Amnon; Ničković, Dejan; Aichernig, Bernhard K.: Bounded determinization of timed automata with silent transitions (2017)
  13. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  14. Benerecetti, Massimo; Peron, Adriano: Timed recursive state machines: expressiveness and complexity (2016)
  15. Camacho, Carlos; Llana, Luis; Núñez, Alberto: Cost-related interface for software product lines (2016)
  16. Wimmer, Simon: Formalized timed automata (2016)
  17. Bouyer, Patricia; Markey, Nicolas; Sankur, Ocan: Robust reachability in timed automata and games: a game-based approach (2015)
  18. Motallebi, Hassan; Azgomi, Mohammad Abdollahi: Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques (2015)
  19. 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) ioport
  20. Andrychowicz, Marcin; Dziembowski, Stefan; Malinowski, Daniel; Mazurek, Łukasz: Modeling Bitcoin contracts by timed automata (2014)

1 2 3 ... 12 13 14 next