Tools and Methods for RTCP-Nets Modeling and Verification

M. Szpyrka; J. Biernacki; A. Biernacka

doi:10.1515/acsc-2016-0019

Tools and Methods for RTCP-Nets Modeling and Verification

Szpyrka, M., Biernacki, J., Biernacka, A.

Source

Archives of Control Sciences > 2016 > Vol. 26, no. 3 > 339--365

Abstract

RTCP-nets are high level Petri nets similar to timed colored Petri nets, but with different time model and some structural restrictions. The paper deals with practical aspects of using RTCP-nets for modeling and verification of real-time systems. It contains a survey of software tools developed to support RTCP-nets. Verification of RTCP-nets is based on coverability graphs which represent the set of reachable states in the form of directed graph. Two approaches to verification of RTCP-nets are considered in the paper. The former one is oriented towards states and is based on translation of a coverability graph into nuXmv (NuSMV) finite state model. The later approach is oriented towards transitions and uses the CADP toolkit to check whether requirements given as μ-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples.

Identifiers

journal ISSN :	1230-2384
DOI	10.1515/acsc-2016-0019

Authors

Szpyrka, M.

AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

Biernacki, J.

AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

Biernacka, A.

AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

Keywords

RTCP-nets Petri nets model checking coverability graphs nuXmv CADP

Additional information

Publication languages: English

Data set: BazTech

Publisher

Polish Academy of Sciences, Committee of Automatic Control and Robotics

Fields of science

No field of science has been suggested yet.

Bibliography

[1] W. M. P. van der Aalst: Interval timed coloured Petri nets and their analysis. In Proc. of the 14th Int. Conf. on Application and Theory of Petri Nets, 691 London, UK, (1993), 453-472.
[2] A. Biernacka, J. Biernacki and M. Szpyrka: State-based verification of RTCP-nets with nuXmv. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100010–1–100010–4.
[3] J. Biernacki, A. Biernacka and M. Szpyrka: Action-based verification of RTCP-nets with CADP. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100011–1–100011–4.

see all

article

Read online
Download
Add to read later
Add to collection
Add to followed
Share

Export to bibliography


Assign to other user
	×
Wrong email address

INFONA - science communication portal

Tools and Methods for RTCP-Nets Modeling and Verification $("#expandableTitles").expandable();

Source

Abstract

Identifiers

Authors

User assignment

Assignment remove confirmation

You're going to remove this assignment. Are you sure?

Szpyrka, M.

Biernacki, J.

Biernacka, A.

Keywords

Additional information

Publisher

Fields of science

Fields of science

Bibliography

[1] W. M. P. van der Aalst: Interval timed coloured Petri nets and their analysis. In Proc. of the 14th Int. Conf. on Application and Theory of Petri Nets, 691 London, UK, (1993), 453-472.

[2] A. Biernacka, J. Biernacki and M. Szpyrka: State-based verification of RTCP-nets with nuXmv. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100010–1–100010–4.

[3] J. Biernacki, A. Biernacka and M. Szpyrka: Action-based verification of RTCP-nets with CADP. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100011–1–100011–4.

Share

Export to bibliography

Reporting an error / abuse

Sending the report failed

Accessibility options

Tools and Methods for RTCP-Nets Modeling and Verification