Give an example for traffic light pedestrian crossing. Example of controlling the machine.

Safety: The requirement of lack of collisions - there shouldn't be green light in the crossed directions

Vivacity: An admission guarantee through the intersection: sometime we will wait for the green

This program is incorrect! How to check a program correctness? Verification of the requirements expressed in language of temporal logic the Task: to change the program until it doesn't meet requirements of a correctness

The choice of a set of the checked formulas is carried out by the person – the verifier, nobody can tell, check is how FULLY carried out – whether everything the necessary properties of system are checked

Introduction of templates helps formalization of requirements to system

Definition of classes of properties allows not to pass some important types of properties at verification

Approachibility some concrete state will be reached (reachability)

Safety: something bad won't occur (safety)

Vivacity: something good will be executed (liveness)

Freedom from dedlok (deadlock freeness, non blocking)

process won't be blocked by other process Justice (fairness):

restriction of unreal or undesirable trajectories

27. How to find the intersection of languages: Finite Automata. Mutual exclusion.

Finite automata:

The language which is crossing of automatic languages it is possible to define, having constructed synchronous composition of final machine guns.

Mutual exclusion: If two or more concurrent processes execute the same code and access the same data, there is a potential problem that they may overwrite each others results and corrupt the data. The mutual exclusion problem is the problem of restricting access to a critical section in the code to a single process at a time, assuming only the indivisibility of read and write instructions.

not executed executed

Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of correctness properties expressed in the syntax of Linear-time Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient on-the-fly verifications procedure.

PROMELA is a process modeling language whose intended use is to verify the logic of parallel systems. Given a program in PROMELA, Spin can verify the model for correctness by performing random or iterative simulations of the modeled system's execution, or it can generate a C program that performs a fast exhaustive verification of the system state space. During simulations and verifications SPIN checks for the absence of deadlocks, unspecified receptions, and unexecutable code. The verifier can also be used to prove the correctness of system invariants and it can find non-progress execution cycles. Finally, it supports the verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic. Each model can be verified with Spin under different types of assumptions about the environment. Once the correctness of a model has been established with Spin, that fact can be used in the construction and verification of all subsequent models. PROMELA programs consist of processes, message channels, and variables. Processes are global objects that represent the concurrent entities of the distributed system. Message channels and variables can be declared either globally or locally within a process. Processes specify behavior, channels and global variables define the environment in which the processes run.

Example: Let’s consider the simple parallel program

process Inc = while true do if x<10 then x:=x+1 od

process Dec = while true do if x>0 then x:=x-1 od

process Reset = whiletrue do if x=10 then x:=0 od

0≤x≤10 processes fulfill the contract? Check it to create a program in Promela:

x=0;

proctype Inc() {

do :: true -> if ::x<10 -> x= x+1 fi od}

proctype Dec() {

do :: true -> if :: x>0 -> x= x-1 fi od}

proctype Reset() {

do :: true -> if :: x==10 -> x= 0 fi od}

proctype Check() {

assert (x>=0&& x<=10)}

init{

atomatic { run Inc(); run Dec(); run Reset(); run Check();

}

Kripke’s structure:

The general description of functioning of the reacting systems:

loop

to read values from entrance sensors

on the basis of the received values to make active affektor

forever

There is a set of the models representing the reacting systems: final machine guns, systems of transitions, Petri's networks, a steytcharta (the card of states), the interacting Milner's machine guns, programs in languages with the variables having limited ranges of definition, etc. Kripke's structure for all of them can be chosen as underlying semantic model.

29. Define modeling systems. “Instantaneity” transitions. Parallel processes: interleaving. Execution of parallel processes with atomic chain operators.

Class of systems – the reacting systems. A subject of the analysis – their behavior. Standard model of the reacting systems are systems of transitions – states and transitions between them. The state describes information on system in some timepoint. Condition of the hardware scheme – a condition of registers and entrances. The condition of the traffic light – what burns light. Atomic predicates – ratios between state parameters. Behavior – (infinite) sequence of states (a trajectory in space of states). State – a set of values of variables and the program counter. Transition – change of a state, for example, performance of the operator of the program.

"Instantaneousness" of transitions:

In temporal logic only the order of events (states) is used. When performing transition the system doesn't pass intermediate states. There is no part of transition. The system passes from a state into a state "instantly". Is accepted that the system was in some stable state, and then passed into another (stable) under the influence of performance of the operator or an event. When performing transition the system doesn't pass intermediate states. There is no part of transition. The system passes from a state into a state "instantly".

We can't use the term "instantly", it is connected with time. Instead of "instantaneousness" we speak about "elementary quality" of transitions.

The Interliving in the parallel program is a nondeterministic choice of an order in which operators of each of processes will be carried out (we abstract from speeds of processes).

Execution of parallel processes with atomic chain operators:

byte state = 1;

proctype A( ) {

atomic { (state==1) -> state = state+1 }

}

proctype B( ) {

atomic { (state==1) -> state = state-1 }

}

init {

run A( ); run B( )

}

Value of the state variable will become equal 2 or 0, depending on what of processes, A or B, the first will execute the atomic operation. Other process thus will be blocked forever.

Date: 2016-01-03; view: 1715