?
On Temporal Properties of Nested Petri Nets
P. 122-127.
Dworzanski L. W., Frumin D. I.
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.
In book
Kamkin A., Petrenko A., Terekhov A. Perm : -, 2012
Rybakov M., Котикова Е. А., Logical Investigations 2015 Vol. 21 No. 1 P. 86-99
For an infinite class of calculi containing CTL and QCL, it is proved that they are Kripke incomplete. ...
Added: July 20, 2020
Tatarnikov A., Kamkin A., Сергеева Т. И. et al., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 51-57 .
Creation of test programs and analysis of their
execution is the main approach to system-level verification of microprocessors. A lot of techniques have been proposed to automate test program generation, ranging from completely random to well directed ones. However, no “silver bullet” has been found. In good industrial practices, various methods are combined complementing each other. ...
Added: December 20, 2017
Tatarnikov A., Kamkin A., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70-74
А method for automated generating test programs for functional testing of single-core microprocessor memory subsystems is proposed. The proposed method is based on formal specifications of the caching and address translation mechanisms. The method variants have been successfully applied to testing of industrial microprocessors. ...
Added: January 25, 2018
Tatarnikov A., Kamkin A., Проценко А. С. et al., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM is a family of microprocessor instruction set architectures developed in a company with the same name. The newest architecture of this family, ARMv8, contains a large number of instructions of various types and is notable for its complex organization of virtual memory, which includes hardware support for multilevel address translation and virtualization. All of ...
Added: November 24, 2017
Samokhvalov D., Dworzanski L. W., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 3 P. 65-84
Nested Petri net formalisms is an extension of coloured Petri net formalism that uses Petri Nets as tokens. The formalism allows creating comprehensive models of multi-agent systems, simulating, verifying and analyzing them in a formal and rigorous way. Multi-agent systems are found in many different fields — from safety critical systems to everyday networks of ...
Added: September 15, 2016
Dworzanski L. W., Lomazova I. A., , in : Application and Theory of Petri Nets and Concurrency. 37th International Conference, PETRI NETS 2016, Toruń, Poland, June 19-24, 2016. Proceedings. Vol. 9698: Lecture Notes in Computer Science.: Switzerland : Springer, 2016. P. 325-344.
Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” approach. Due to tokens with individual behavior and the mechanism of synchronization NP-nets are convenient for modeling multi-agent and adaptive systems, flexible workflow nets, and other systems with mobile interacting components and dynamic structure. In contrast to classical Petri nets, ...
Added: June 11, 2016
Dworzanski L. W., Lomazova I. A., , in : Program Semantics, Specification and Verification: Theory and Applications. The conference materials. : Nizhny Novgorod : Nizhny Novgorod State University, 2012. P. 55-63.
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 ...
Added: September 21, 2012
Mitsyuk A. A., Котылев Я. В., , in : Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected Papers. Vol. 779: Communications in Computer and Information Science.: Springer, 2018. Ch. 11. P. 127-138.
Modern software systems can be large. They often have a complex architecture and non-trivial behaviour. That is why different modelling techniques are used for their design and analysis. Illustrative visualization of a system architecture can facilitate better analysis and give useful insights. In this paper we propose an approach for visualization of software system models. ...
Added: January 30, 2018
Tatarnikov A., Kamkin A., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
A memory subsystem is one of the key components of a microprocessors. It consists of a number of storage devices (instruction buffers, address translation buffers, multilevel cache memory, main memory, and others) organized into a complex hierarchical structure. Huge state space of a memory subsystem makes its functional verification extremely labor consuming. Nowadays, the main ...
Added: December 10, 2017
Tatarnikov A., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
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 ...
Added: February 2, 2018
Rybakov M., Чагрова Л. А., Программные продукты и системы 2018 Т. 31 № 3 С. 591-597
It is common to use the first-order language as a formal tool for describing properties of various (computational) structures. On the one hand, this language is well understood and easy to use; on the other, many questions that are im-portant from the applications point of view related to this language are algorithmically undecidable, i.e., cannot ...
Added: October 6, 2019
Tatarnikov A., Kamkin A., , in : Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer Science. Vol. 10742.: Springer, 2018. P. 387-393.
The paper presents MicroTESK, a tool for test program generation for functional verification of microprocessors. It generates test programs from templates which describe generation tasks in terms of constraints that must be satisfied in order to reach certain coverage goals. The tool uses formal specifications of the instruction set as a source of knowledge about ...
Added: January 23, 2018
Buchina N. G., Dworzanski L. W., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 15-18.
The work provides a specific approach to modeling and simulating Wireless Sensor Networks (WSN) via nested Petri Nets formalism. The tool for modeling/simulating WSN must take into account resources, time and sensors cost. Even though classical Petri Nets are well-suited for modeling dynamic concurrent systems, they do not have enough expressibility to model systems with ...
Added: July 4, 2013
Humboldt-Universität zu Berlin, 2016
This volume contains the papers presented at CS&P 2016, the 25th International Workshop on Concurrency, Specification and Programming, held on September 28 - 30, 2016 in Rostock, Germany. Since the early seventies Warsaw University and Humboldt University have alternately organized an annual workshop - since the early nineties known as CS&P. Over time, it has ...
Added: October 13, 2016
Л. В. Дворянский, И. А. Ломазова, Программирование 2016 № 5 С. 49-67
Multi-agent systems (MAS) with many levels and dynamic hierarchical structure are widely used in telecommunication, transport, social, and other fields.
Assuring correctness of such systems is an important and topical issue.
In this paper we consider modeling MAS with dynamic structure with the help of Nested Petri nets (NPNs). NPN is an extension of Petri nets within ...
Added: December 4, 2015
Dworzanski L. W., , in : Formal Modeling and Analysis of Timed Systems. Vol. 9884.: Switzerland : Springer, 2016. Ch. 1. P. 3-18.
The nested Petri nets are a nets-within-nets formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. The formalism is supported by developed verification methods based on structural analysis and model checking techniques. Time constraints are crucial for many safety critical and everyday IoT systems. Recently, the non Turing-complete time semantics ...
Added: September 13, 2016
Ermakova V., Lomazova I. A., Труды Института системного программирования РАН 2016 Т. 28 № 4 С. 115-136
Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model ...
Added: October 21, 2016
Dworzanski L. W., Frumin D. I., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 9-14.
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 ...
Added: June 18, 2013
Tatarnikov A., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Test program generation and simulation is the most widely used approach to functional verification of microprocessors. Functional verification is a quite time consuming process. According to various estimates, it accounts for more than 70% of overall resources spent on designing a new microprocessor. This can be explained by the fact that modern hardware designs have ...
Added: December 12, 2017
Dworzanski L. W., Lomazova I. A., , in : Program Semantics, Specification and Verification: Theory and Applications. The conference materials. 6th International Computer Science Symposium in Russia. : Yaroslavl : Yaroslavl State University, 2011. P. 27-34.
Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level Nested Petri nets (NP-nets). Boundedness and liveness are still very hard to check even for plain Petri nets (EXPSPACE or worse). For the restricted class of free-choice Petri nets some problems become more amenable to analysis. ...
Added: March 23, 2013
Tatarnikov A., Kamkin A., Чупилко М. М. et al., , in : Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science. Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham : Springer, 2017. P. 217-220.
The paper presents MicroTESK, a tool that automates construction of test program generators for microprocessors. A constructed generator consists of the core that implements architecture-independent generation methods and the model that holds information required to generate tests for the corresponding architecture. The tool extracts this information from formal specifications of the instruction set architecture. The ...
Added: January 24, 2018
Tatarnikov A., , in : Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). : Yerevan : IEEE, 2016. P. 270-273.
The paper proposes an approach to instruction stream generation for verification of microprocessor designs. The approach is based on using formal specifications of the instruction set architecture as a source of knowledge about the design under verification. This knowledge is processed with generic engines implementing an extensible set of generation strategies to produce stimuli in ...
Added: December 22, 2017