Download Logics and Models of Concurrent Systems PDF

TitleLogics and Models of Concurrent Systems
Author
LanguageEnglish
File Size18.4 MB
Total Pages493
Document Text Contents
Page 1

Logics and Models of Concurrent Systems

Page 2

NATO ASI Series
Advanced Science Institutes Series

A series presenting the results of activities sponsored by the NA TO Science Committee,
which aims at the dissemination of advanced scientific and technological knowledge,
with a view to strengthening links between scientific communities.

The Series is published by an international board of publishers in conjunction with the
NATO Scientific Affairs Division

A Life Sciences
B Physics

C Mathematical and
Physical Sciences

D Behavioural and
Social Sciences

E Applied Sciences

F Computer and
Systems Sciences

G Ecological Sciences

Plenurn Publishing Corporation
London and New York

D. Reidel Publishing Company
Dordrecht, Boston and Lancaster

Martinus Nijhoff Publishers
Boston, The Hague, Dordrecht and Lancaster

Springer-Verlag
Berlin Heidelberg New York Tokyo

Series F: Computer and Systems Sciences Vol. 13

Page 246

243

Example: Consider [P II Q II R] declared by:

process P; int x; boo) c; process Q
proc pr begin call P.pr end

begin x:=x+1; c:= -c;
when c:skip end

end
begin x:=O;c:= true end

process R
begin call P.qr end

We sketch the proof of { true} [P II Q II R] {x=l}.
Only application of the external request rule between Q and P, and the Iff of PIp: at('w')

over pr.body is shown. The following proof outlines are used:

. process Q
process P; mt .x; boo) c {h=O} begin

proc pr begm h:=1> < h:=1; call P.pr >
{1i=1 A x=O} x:=x+1; c:=-c {x=1 A 1i=1}end {h=1}

'W': when c: skip end {x=1}
< end {x=h}
proc qr begin c: = - c end

{1i=O} begin x:=O; c:= true end {x=li}

GI == h=1i A pr'inc ~ h

PIp == MIp A (at(pr): x=O A Ii = 1) A (after(pr): x=l) A (at('w'): x=l A h=l)

MIp == x=1i

In order to apply the external request rule for call P.pr, its three clauses need to be checked:

first clause: {h=O A x=1i A h=li. A pr'inc ,..h }
P A MIp A GI

h:=1. pr'inc'= pr'inc+1' h:=1
SI" , TI[%]

{h=1 A A=1 A x=O A h=A A pr'inc ,.. h }
P;- A PI:at(pr)[%] A GI '

which is clearly correct.

second clause: {x=O A 1i=1} x:=x+1; c:= ~c; when c: skip end {x=l}

third clause: {h=l A x=l A h=1i A pr'inc ~ h}

~. pr'inc'= pr'inc-1' skip
T2[%]" , S2

{h=l A x=1i A h=1i A pr'inc ~ h}

Page 247

244

IFf of PI: at('w') over pr.body, with p = atCW') and S = pr.body:
INV(p,S) requires proof of

{x=l A h=l A x=O A h=lA .. ·ts fX=lJ
p('1i:l') A PI: at(pr)

false

x=l A h=l A x=l A h=l A b=h A pr'ine ~ h ,. 2

with PI' = at('w'): P A PI:at('W') A GI Apr me '"
false

This proof is trivial indeed:

{false} x:=x+l; c:=-c; {false} when c: skip end {x=l} is obviously a valid proof outline,

because the first clause of the when rule requires proving {false 1\ c} skip {x= I}, and the
second and third clause are equally trivial, PI' being false.
D

A nontrivial example, the dutch national torus, has been given in [GdeRR02] and is

reproduced in the appendix; the problem, "inspired by the Dutch National Flag", originally

appeared in Dijkstra's [EWD 608] in a version written in CSP.

A correctness proof of a distributed priority queue has been given in [GdeRRol], concerning

a program given in Brinch Hansen's original DP article [BH]. When trying to prove this

program an error was discovered, which was subsequently mended.

6. References

[ARM]

[Apt 1]

Utrecht, "Christmas holidays 84/85"

ADA, The Programming Language ADA Reference Manual, LNCS 155

(1983).

Apt, K.R., Ten Years of Hoare's Logic - Part I, Toplas 3 (1981),

431-484.

Page 492

498

Now, clearly 8 is not a legal statification of 8 j in general, since it
refers to elements from E - E j . However, this can be fixed as follows.
Output elements in E - Ej are simply eliminated, and for each input ele-
ment e therein one finds a k with e E Ek, and modifies the two copies of
8, that of Ek and that of Ej, so that the former, whenever e is sensed,
outputs a new item e' to Mj, in whose copy of 8 each e is replaced by e'.
In this way M j can sense the input event e even though it can be directly
sensed only by Mk • The resulting statecharts, call them 8f, ... , 8:, are
now legel behavioral specifications of the M j , in the sense that their or-
thogonal product is equivalent to 8. Moreover, the 87 are on the same
horizontal level of detail as 8. These 87, therefore, conform to the def-
inition of the preliminary description of S,eHl), see Fig. 12, and hence,
in principle, we have answered question (2). However, we clearly do not
recommend that one stop here; the result will be an exponentially grow-
ing behavioral specification, not to mention its complete detachment from
any naturalness involved in the implementation refinement of M into the
Mj. Rather, one should work on the 87, simplifying and changing them
to reflect the intended behavior of the Mj. In this sense, the only useful
role 87 can play, is that of a starting point leading to the desired Sj, the
final behavioral specification of Mj.

Actually, we feel that it is worthwhile to search for good transforma-
tions for weeding out portions of 87 not really relevant to Mj, using the
difference between E and Ej, and S itself as directives. Such transforma-
tions, certain simple examples of which come immediately to mind, should
be required to preserve equivalence of the behavior, modulu the transition
from E to E j .

The equivalence problem for reactive behavioral specifications, and in
particular equivalence-preserving transformations of statecharts, seems to
be an important area for future research. Satisfactory and useful results
in this direction can help turn the magic square from a model of system
development, which is the way we have tried to portray it here, into a de-
tailed methodology, or prescription, a line we have not yet tried to pursue.

Acknowledgement

The contents of this paper owe IDuch to IDany colleagues and authors.
In particular, we have been influenced by several ideas found in the work
of M. Alford, L. Lamport and D. Parnas.

Page 493

NATO ASI Series F

Vol. 1. Issues in Acoustic Signal-Image Processing and Recognition. Edited by C. H. Chen. VIII, 333
pages. 1983.

Vol. 2 Image Sequence Processing and Dynamic Scene Analyisi. Edited by 1 S. Huang. IX, 749
pages. 1983.

Vol. 3 Electronic Systems Effectiveness and Life Cycle Costing. Edited by J. K. Skwirzynskl. XVII, 732
pages. 1 983.

Vol. 4. Pictorial Data Analysis. Edited by R. M. HarallCk. VIII, 468 pages. 1983.

Vol. 5 International Calibration Study of Traffic Conflict Techniques. Edited by E. Asmussen VII, 229
pages. 1984.

Vol. 6 Information Technology and the Computer Network. Edited by K. G. Beauchamp. VIII, 271
pages. 1984.

Vol. 7. High-Speed Computation. Edited by J. S. Kowalik. IX, 441 pages. 1984.

Vol. 8. Program Transformation and Programming Environments. Report on an Workshop directed by
F. L. Bauer and H. Remus. Edited by P Pepper. XIV, 378 pages. 1984.

Vol. 9 Computer Aided Analysis and Optimization of Mechanical System Dynamics. Edited by E. J.
Haug. XXII, 700 pages. 1984.

Vol. 10 Simulation and Model-Based Methodologies An Integrative View. Edited by 1 I. Oren, B. P
Zeigler, M. S. Elzas. XIII, 651 pages. 1984.

Vol. 11. Robotics and Artificial Intelligence. Edited by M. Brady, L. A Gerhardt, H. F. Davidson. XVII, 693
pages. 1984.

Vol. 12 Combinatorial Algorithms on Words. Edited by A Apostolico, Z. Galil. VIII, 361 pages. 1985.

Vol. 13 Logics and Models of Concurrent Systems. Edited by K. R. Apt. VIII, 498 pages. 1985.

Similer Documents