Pregled bibliografske jedinice broj: 124193
Modeliranje Petrijevom mrežom za verifikaciju reaktivnih sustava
Modeliranje Petrijevom mrežom za verifikaciju reaktivnih sustava // Proceedings of the 7th International Conference on Telecommunications / Jevtić, Mikuc (ur.).
Zagreb: Fakultet elektrotehnike i računarstva Sveučilišta u Zagrebu, 2003. str. 257-264 (poster, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
CROSBI ID: 124193 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Modeliranje Petrijevom mrežom za verifikaciju reaktivnih sustava
(Petri Net Modeling for Reactive System Verification)
Autori
Blašković, Bruno
Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni
Izvornik
Proceedings of the 7th International Conference on Telecommunications
/ Jevtić, Mikuc - Zagreb : Fakultet elektrotehnike i računarstva Sveučilišta u Zagrebu, 2003, 257-264
Skup
ConTEL 2003
Mjesto i datum
Hrvatska, 11.06.2003. - 16.06.2003
Vrsta sudjelovanja
Poster
Vrsta recenzije
Međunarodna recenzija
Ključne riječi
sustav u stvarnom vremenu; verifikacija; Petrijeva mreža; Elementarni komunicirajući procesi; CO4pe metamodel
(Real-time system; model checking; Petri nets; Elementary Communicating Processes; CO4pe metamodeling framework)
Sažetak
Verification methodologies like model checking and theorem proving are important part of complex system design. Correct behaviour of concurrent reactive real-time system is among other constraints also time dependable. This paper sublimes modeling efforts in order to bridge the gap between concurrent software, model checking tools, models of computations and formal specifications. The development of a model checking input code from the formal specification or source code can produce hundreds lines of code. In order to automatize such a task, here introduced as model extracting, the experimental meta-modeling framework is developed to bridge semantical differences between various software verification tools on one, and between system description on the other side. Modeling framework is an environment where the model for experimenting with the problem solution is built. The model consists of interconnected Elementary Communicating Processes (ECP). An interpretation of interconnections reflects the model of computation used: object oriented, Petri Net, communicating reactive automata, component and coordination models, intelligent agents ... ECP are grouped on three levels of abstraction to benefit from theoretical backgrounds like process algebras or high level Petri nets. Roughly speaking, model is the collection of connected tools and modeling is the proces of tool integration. Further on, after the presentation of some related approaches, meta-modelling framework is introduced through Petri net model together with illustrative example.
Izvorni jezik
Engleski
Znanstvena područja
Elektrotehnika
