hrcak mascot   Srce   HID

Journal of computing and information technology, Vol. 17 No. 3, 2009.

Izvorni znanstveni članak
https://doi.org/10.2498/cit.1001272

Verification of Complex Real-time Systems using Rewriting Logic

Mustapha Bourahla

Puni tekst: engleski, pdf (320 KB) str. 265-284 preuzimanja: 416* citiraj
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.

Hrčak ID: 44865

URI
https://hrcak.srce.hr/44865

Posjeta: 602 *