scholarly journals Verification of Compliance for Multilevel Models in Individual Trace Semantics

2020 ◽  
Vol 32 (6) ◽  
pp. 19-30
Author(s):  
Alexey Vladimirovich Khoroshilov
Keyword(s):  
Multilevel Models ◽  
Transition System ◽  
Abstract Model ◽  
Detailed Model ◽  
Industrial Systems ◽  
Reasonable Approach ◽  
Trace Semantics ◽  
Initial States ◽  
Verification Techniques ◽  
Labelled Transition System

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.

scholarly journals Verification of Compliance for Multilevel Models in Individual Trace Semantics

2020 ◽  
Vol 32 (6) ◽  
pp. 19-30
Author(s):  
Alexey Vladimirovich Khoroshilov
Keyword(s):  
Multilevel Models ◽  
Transition System ◽  
Abstract Model ◽  
Detailed Model ◽  
Industrial Systems ◽  
Reasonable Approach ◽  
Trace Semantics ◽  
Initial States ◽  
Verification Techniques ◽  
Labelled Transition System

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.

scholarly journals Study on Formal Modeling and Safety Verification of Train-to-Train Communication

2018 ◽  
Vol 2018 ◽  
pp. 1-9
Author(s):  
Haonan Feng
Keyword(s):  
Transition System ◽  
Research Trend ◽  
Safety Properties ◽  
Safety Verification ◽  
Critical System ◽  
Real Time System ◽  
Vehicle Communication ◽  
Train Control ◽  
Safety Critical System ◽  
Labelled Transition System

VBTC (vehicle-to-vehicle communication based train control) has gradually become an important research trend in the field of rail transit. This has resulted in advantages of decreasing the number of pieces of wayside equipment and improving the efficiency of real-time system communication. Characteristics and mechanism of train-to-train communication, as key implementation technology of safety critical system, are given and discussed. A new method, based on the LTS (labelled transition system) model checking, is proposed for verifying the safety properties in the communication procedure. The LTS method is adapted to model system behaviours; analysis and safety verification are checked by means of LTSA (labelled transition system analyzer) software. The results show that it is an efficient method to verify safety properties, as well as to assist the complex system’s design and development.

Target-oriented Petri Net Synthesis

2020 ◽  
Author(s):  
Eike Best ◽  
Raymond Devillers ◽  
Evgeny Erofeev ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Transition System ◽  
Efficient Synthesis ◽  
Transition Systems ◽  
Np Complete ◽  
Full Class ◽  
Petri Net Synthesis ◽  
Labelled Transition System ◽  
Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

scholarly journals Boxed ambients with communication interfaces

2007 ◽  
Vol 17 (4) ◽  
pp. 587-645 ◽  
Author(s):  
PABLO GARRALDA ◽  
EDUARDO BONELLI ◽  
ADRIANA COMPAGNONI ◽  
MARIANGIOLA DEZANI-CIANCAGLINI
Keyword(s):  
Information Exchange ◽  
Transition System ◽  
Communication Policy ◽  
Reduction Property ◽  
The Subject ◽  
Communication Policies ◽  
Ambient Calculus ◽  
Labelled Transition System

We define BACI(Boxed Ambients with Communication Interfaces), an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy determining the kind of information that can be exchanged with a parent ambient, even though mobility changes the parent. BACI lifts that restriction, allowing different communication policies with different parents during computation. Furthermore, BACI separates communication and mobility by making the channels of communication between ambients explicit. In contrast with other typed ambient calculi where communication policies are global, each ambient in BACI is equipped with a description of the communication policies ruling its information exchange with parent and child ambients. The communication policies of ambients increase when they move: more precisely, when an ambient enters another ambient, the entering ambient and the host ambient can exchange their communication ports and agree on the kind of information to be exchanged. This information is recorded locally in both ambients.We show the type-soundness of BACI, proving that it satisfies the subject reduction property, and we study its behavioural semantics by means of a labelled transition system.

scholarly journals A Semantic Theory for Value-Passing Processes Based on the Late Approach

2003 ◽  
Vol 10 (15) ◽  
Author(s):  
Anna Ingólfsdóttir
Keyword(s):  
General Class ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Theory ◽  
Transition System ◽  
Semantic Approach ◽  
Proof Systems ◽  
A Value ◽  
Concrete Language ◽  
Labelled Transition System

A general class of languages for value-passing calculi based on the late semantic approach is defined and a concrete instantiation of the general syntax is given. This is a modification of the standard CCS according to the late approach. Three kinds of semantics are given for this language. First a Plotkin style operational semantics by means of an applicative labelled transition system is introduced. This is a modification of the standard labelled transition system that caters for value-passing according to the late approach. As an abstraction, late bisimulation preorder is given. Then a general class of denotational models for the late semantics is defined. A denotational model for the concrete language is given as an instantiation of the general class. Two equationally based proof systems are defined. The first one, which is value-finitary, i. e. only reasons about a finite number of values at each time, is shown to be sound and complete with respect to this model. The second proof system, a value-infinitary one, is shown to be sound with respect to the model, whereas the completeness is proven later. The operational and the denotational semantics are compared and it is shown that the bisimulation preorder is finer than the preorder induced by the denotational model. We also show that in general the omega-bisimulation preorder is strictly included in the model induced preorder. Finally a value-finitary version of the bisimulation preorder is defined and the full abstractness of the denotational model with respect to it is shown. It is also shown that for CCS_L the omega -bisimulation preorder coincides with the preorder induced by the model. From this we can conclude that if we allow for parameterized recursion in our language, we may express processes which coincide in any algebraic domain but are distinguished by the omega-bisimulation. This shows that if we extend CCS_L in this way we obtain a strictly more expressive language.

scholarly journals Labelled transition system approach to distributed computing systems

2016 ◽  
Vol 8 (3) ◽  
pp. 19-32
Author(s):  
Dang Van Hung
Keyword(s):  
Distributed Computing ◽  
System Approach ◽  
Transition System ◽  
Distributed Computing Systems ◽  
Computing Systems ◽  
Transition Systems ◽  
Local Process ◽  
Global Properties ◽  
Labelled Transition System

The present paper introduces the  notion of  distributed transition systems for modeling, designing and  understanding distributed computing systems. The concurrency can be expressed explicitly in the model. Some of  the  global properties of the  systems are discussed and determined. It is  shown in the paper that  by keeping knowledge of other processes in each process of a system, some of its global properties can be synthesized from only few local process states.

Sign in / Sign up

Export Citation Format

Share Document