On Temporal Properties of Nested Petri Nets
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw and Humboldt Universities, as Polish-German annual meetings. They were suspended for some years in the 1980s and reactimed in 1992. Thereafter, the Workshop, organised alternatingly by the Institutes of Informatics and Mathematics of the University of Warsaw and the Institute of Informatics of Humboldt University in Berlin on the basis of an exchange program, has been given the name GS&P. It should be mentioned that the CS&P meetings, initially purely bilateral, since 1992 have developed into events attended by participants from a number of different countries beside Poland and Germany. The present GS&P'13 meeting attracted contributors from: Canada, Egypt, France, Germany, Italy, Nepal, The Netherlands, Poland, Russia, Serbia, Slenakia, Sweden, Turkey, United Kingdom, United States, and Vietnam. The organisation of this year's CS&P would not be possible without the resources and financing provided by seven institutions. We would like to thank the Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw and the Institute of Informatics of the Humboldt University of Berlin for the continuing financial and organisational support provided to GS&P over last twenty-two years. The essential financial backing received from the Warsaw Center of Mathematics and Computer Science made the organisation of CS&P 2013 possible. Our thanks go to the Bialystok University of Technology for providing the means for publishing this proceedings volume. Last, but not the least, we are grateful for the significant financial support provided by the Vistula University in Warsaw.
Nested Petri nets (NP-nets) is an extension of Petri net formalism within the “nets-within-nets” approach, when tokens in a marking are Petri nets wich have autonomous behavior and synchronize with the system net. The formalism of NP-nets allows modeling multilevel multiagent systems with dynamic structure in a natural way. Currently there is no tool support for NP-nets simulation and analysis. The paper proposes translation of NP-nets into colored Petri nets and using CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.
Nested Petri nets (NP-nets) are Petri nets with net tokens - an extension of high-level Petri nets for modeling active objects, mobility and dynamics in distributed systems. In this paper we present an algorithm for translating two-level NP-nets into behaviorally equivalent Colored Petri nets with the view of applying CPN methods and tools for nested Petri nets analysis. We prove, that the proposed translation preserves dynamic semantics in terms of bisimulation equivalence.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar to a meeting attended also by colleagues from other countries than Poland and Germany. This year there are 34 participants from 10 countries.
Software-dened networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was dened in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specication of SDN forwarding policies, and set up formally model-checking problems for SDNs.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. While having a number of interesting properties, NP-nets have been lacking tool support. In this paper we present the NPNtool toolset for NP-nets which can be used to edit NP-nets models and check liveness in a compositional way. An algorithm to check m-bisimiliarity needed for compositional checking of liveness has been developed. Experimental results of the toolset usage for modelling and checking liveness of classical dinning philosophers problem are provided.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and verication, programming and specification languages, etc.
The paper proposes a method of automated construction of behavior models of microprocessors, which are used in the process of test program generation to predict the results. The proposed method is based on using formal specifications of instruction set architecture. The method is implemented in MicroTESK, a test program generation tool being developed at ISP RAS. The tool has been successfully applied in industrial projects.