APA 6th Edition Bourahla, M. (2009). Verification of Complex Real-time Systems using Rewriting Logic. Journal of computing and information technology, 17 (3), 265-284. https://doi.org/10.2498/cit.1001272
MLA 8th Edition Bourahla, Mustapha. "Verification of Complex Real-time Systems using Rewriting Logic." Journal of computing and information technology, vol. 17, br. 3, 2009, str. 265-284. https://doi.org/10.2498/cit.1001272. Citirano 04.03.2021.
Chicago 17th Edition Bourahla, Mustapha. "Verification of Complex Real-time Systems using Rewriting Logic." Journal of computing and information technology 17, br. 3 (2009): 265-284. https://doi.org/10.2498/cit.1001272
Harvard Bourahla, M. (2009). 'Verification of Complex Real-time Systems using Rewriting Logic', Journal of computing and information technology, 17(3), str. 265-284. https://doi.org/10.2498/cit.1001272
Vancouver Bourahla M. Verification of Complex Real-time Systems using Rewriting Logic. Journal of computing and information technology [Internet]. 2009 [pristupljeno 04.03.2021.];17(3):265-284. https://doi.org/10.2498/cit.1001272
IEEE M. Bourahla, "Verification of Complex Real-time Systems using Rewriting Logic", Journal of computing and information technology, vol.17, br. 3, str. 265-284, 2009. [Online]. https://doi.org/10.2498/cit.1001272
Sažetak This paper presents a method for model checking dense complex real-time systems. This approach is implemented at the meta level of the Rewriting Logic system Maude. The dense complex real-time system is specified using a syntax which has the semantics of timed automata and the property is specified with the temporal logic TLTL (Timed LTL). The well known timed automata model checkers Kronos and Uppaal only support TCTL model checking (a very limited fragment in the case of Uppaal). Specification of the TLTL property is reduced to LTL and its temporal constraints are captured in a new timed automaton. This timed automaton will be composed with the original timed automaton representing the semantics of the complex real-time system under analysis. Then, the product timed automaton will be abstracted using partition refinement of state space based on strong bi-simulation. The result is an untimed automaton modulo the TLTL property which represents an equivalent finite state system to be model checked using Maude LTL model checking. This approach is successfully tested on industrial designs.