Paper Info
Title
ROSECON: a Computer Tool for Synthesis and Verification of Concurrent Systems Specified by Information Systems
Abstract
In the paper, a computer tool called ROSECON, used for modeling and analyzing systems of concurrent processes, is described. A special attention is focused on synthesis and verification of concurrent systems specified by information systems. Two kinds of models, synchronous and asynchronous, are considered. In the first approach, all processes included in the modeled system are synchronized globally whereas in the second one, each process is synchronized individually. The presented tool allows generating automatically an appropriate model of a system of concurrent processes, in the form of colored Petri nets, from the specification given by an information system. Analysis of the model behaviors enables users to verify the correctness and/or optimality of the obtained models and to provide some modification procedures to get correct and/or more optimal solutions. Examples of selected well known problems in concurrency, in the paper, emphasize usefulness of the tool in the designing systems of concurrent processes.
Year
DOI
Venue
2013
10.3233/FI-2013-885
Fundam. Inform.
Keywords
Field
DocType
automation,petri nets
Information system,Asynchronous communication,Petri net,Computer science,Concurrency,Correctness,Colored petri,Automation,Computer tools,Distributed computing
Journal
Volume
Issue
ISSN
126
4
0169-2968
Citations 
PageRank 
References 
0
0.34
17
Authors
2
Name
Order
Citations
PageRank
Zbigniew Suraj150159.96
Krzysztof Pancerz223142.30