##### 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.

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.