当前位置:首页 >> >> REVISITING THE TRAFFIC LIGHTS B CASE STUDY

REVISITING THE TRAFFIC LIGHTS B CASE STUDY

RE CH ER C H E

R

E N

IN ST IT UT

I

REVISITING THE “TRAFFIC LIGHTS” B CASE STUDY MIREILLE DUCASS? , LAURENCE ROZ?

ISSN 1166-8687

DE

IN F O

E U Q TI A M R

I

ET

ES ?M T YS S

S

S RE OI T ?A AL

A

PUBLICATION INTERNE No 1424

IRISA
CAMPUS UNIVERSITAIRE DE BEAULIEU - 35042 RENNES CEDEX - FRANCE

INSTITUT DE RECHERCHE EN INFORMATIQUE ET SYST?MES AL?ATOIRES Campus de Beaulieu – 35042 Rennes Cedex – France Tél. : (33) 02 99 84 71 00 – Fax : (33) 02 99 84 71 71 http://www.irisa.fr

Revisiting the \Tra c lights" B case study
Mireille Ducasse* , Laurence Roze **

Themes 2 et 3 | Genie logiciel et calcul symbolique | Interaction homme-machine, images, donnees, connaissances Projets Lande et A da Publication interne n 1424 | Novembre 2001 | 24 pages

Abstract: In the class room, the two important B notions of re nement and implementa-

tion are best illustrated with a whole B system, with machine importation. However, whole systems are often quite di cult to grasp and students are lost in details. The tra c light case study presents a whole application easy to understand. The presented version revises in depth the case study of Chauvet which was hard-coded for the French tra c lights. It could not be easily generalized to model the German or the English tra c lights. As a consequence, it did not give su cient credit to the re nement process. In this report, intrinsic properties of crossroads and tra c lights are speci ed separately. Data re nement and reduction of non determinism are used stepwise. Thanks to this methodology, only the last re nement of the tra c light abstract machine needs a single minor adaptation to address either the German, the French, or the English lights. In 6 supervised hours students can grasp the main features of re nement invariants, data re nement, reduction of non-determinism and importation. Key-words: B formal method, pedagogical case study, re nement, implementation, importation
(Resume : tsvp)
* **

IRISA/INSA ; email : Mireille.Ducasse@irisa.fr IRISA/INSA ; email : Laurence.Roze@irisa.fr

Centre National de la Recherche Scienti?que (UPRESSA 6074) Université de Rennes 1 – Insa de Rennes

Institut National de Recherche en Informatique et en Automatique – unité de recherche de Rennes

Resume : Pour l'apprentissage de la methode formelle B, les deux notions importantes

Etude de cas en B : le feu tricolore revisite

que sont le ra nement et l'implementation necessitent un systeme complet avec importation de machines. Cependant, les systemes complets sont souvent di ciles a apprehender et les etudiants sont perdus dans les details. L'etude de cas du feu tricolore presente une application complete facile a comprendre. La version presentee ici revise en profondeur celle de Chauvet qui codait en dur les feux tricolores francais. On ne pouvait pas la generaliser pour modeliser les feux anglais ou allemands. En consequence elle donnait une image ternie du processus de ra nement. Dans ce rapport les proprietes intrinseques du carrefour et des feux sont speci ees separement. Le ra nement de donnees et la reduction du non-determinisme sont utilises pas a pas. Gr^ce a cette methodologie, seul le dernier ra nement de la machine a abstraite representant le feu necessite une adaptation mineure pour prendre en compte les feux francais, anglais ou allemands. En 6 heures de travaux diriges les etudiants peuvent ainsi apprehender les principes des invariants de liaison des ra nements, les principes du ra nement de donnees, de la reduction du non-determinisme et de l'importation. Mots cles : Methode formelle B, etude de cas pedagogique, ra nement, implementation, importation

\Tra c lights" B case study

3

1 Introduction
The notion of re nement is central to the programming activity 1, 5, 6], and is especially important in a B course. Re nement is hard to understand without implementation, and implementation is hard to understand without importation. Importation seems to be best understood with an example of a whole B system. However, whole systems are often quite di cult to grasp and students are lost in details. The tra c light case study presents a whole application easy to understand. Chauvet speci es in B a crossroad with two crossing roads 2]. However, besides the fact that the initial article is in French, it su ers from two technical problems. Firstly, the level of abstraction seems too low for the speci cation of the crossroad. Indeed, the cycle of colors to be used by the tra c lights are speci ed at the top-level of the crossroad. As the crossroad can operate even without any lights, there must be some intrinsic properties independent of the tra c lights. Secondly, and strongly correlated with the rst point, neither the German nor the English tra c lights can be modeled in Chauvet's abstract machine. Indeed, the three lights have a di erent cycle of colors. The German cycle of colors is red ! yellow ! green ! yellow ! red. The French cycle is red ! green ! yellow ! red. The English cycle is red ! yellowand-red ! green ! yellow ! red. The French cycle is so much hard-coded in Chauvet's case study that the yellow (or yellow-and-red) after red cannot be integrated without changing the whole of the abstract machines. As a consequence, Chauvet does not give su cient credit to the re nement process. In the following, we give a totally revised version of the crossroad abstract machine where the above two problems are xed: intrinsic properties of the crossroad are speci ed independently of the tra c lights, and the implementation of the tra c light abstract machine needs only a single minor adaptation to address either the German, the French, or the English lights. As in Chauvet's case study, we do not address the possible failures. For example, neither the total shutdown of the crossroad for repair, nor the failures of the lamps of the tra c lights are taken into account. This would require much more space than allocated for this article. Our case study contains 16 machines. They have been checked using the \Atelier B" 4]. 416 proof obligations have been produced, of which 308 have been discharged automatically. The remaining 108 proof obligations were straightforward to discharge, 64 were solved by simply asking the interactive prover to prove them (\pr"), 15 were solved with the simplication set command (\ss"), 1 was a proof by contradiction (\ct'), 18 were easy proofs that an element belonged to a set, the last 10 proofs regarded simple function and relation properties. The abstract machines correspond to 1215 lines of B, from which 1530 lines of C++ have been automatically generated. This executable code has been integrated in a Java graphical simulator. Once all the proofs were made, the code ran correctly at the rst try. The case study has been added to the B course described in 3] to illustrate re nement and implementation. Our case study has the advantage of simplicity. Students have no di culty

PI n 1424

4

Ducasse & Roze

A B B B

A C B B

A B C A A

B C D A E

B C D

A 1. Two roads (2 to 4 lanes) 2. Two roads (2 or 3 lanes)

Figure 1: Some crossroads taken into account by our requirements

3. Three roads (3 to 6 lanes)

4. Four roads (4 lanes)

5. Five roads (5 lanes)

understanding the problem to be solved and the overall architecture is small enough to be quickly integrated. The global architecture is given to the students together with the text of this article; the machines have to be lled. The proof obligations of two re nements and one implementation have to be calculated by hand and informally proved. In 6 supervised hours students can grasp the main features of re nement invariants, data re nement, reduction of non-determinism and importation. Section 2 speci es the requirements of a crossroad and of a tra c light monitor. Section 3 gives an overview of the architecture of the system. Sections 4.1 to 4.13 present in details all the machines to specify a crossroad with two roads.

2 Requirements
In this section we present the basic requirements of the failure-free functioning of crossroads and tra c lights. These requirements are kept as abstract as possible. In particular, we introduce the colors only as properties of tra c lights, and not of the crossroad.

2.1 Crossroad requirements

As opposed to Chauvet's speci cation, our requirements do not make any assumption on the number of crossing roads. All the crossroads presented in Figure 1 are modeled. For roads which continue on the other side of the crossroad (as in Figure 1.1 to 1.3) there can be two tra c lanes going in two di erent directions (one in each direction). However, in this case, both lanes have the same rights to cross, or the obligation to stop, at the same time. We therefore only consider the roads and not the lanes. For example, in Figure 1.1 we only consider the two roads; the fact that there are possibly 4 lanes does not have any impact on our design. In Figure 1.5 we consider the ves roads because each lane has di erent crossing rights. Figure 2 summarizes the intrinsic properties of a crossroad, in particular in terms of the usual criteria of availability, safety, and fairness. The crossroad is composed of a number of roads which cross each other. It can be regulated, for example by tra c lights or by a policeman. If this is the case, it is known by the system. At least one road can cross.

Irisa

\Tra c lights" B case study

5

Otherwise the cross road is safe but not very useful. No more than one road can cross at a given time. Before switching the crossing right from one road to another, the crossroad must be clear of vehicles. Otherwise the crossroad is not safe. Each road can cross in turn. Otherwise, the crossroad is safe and useful but not fair. Note that these properties apply even without any tra c light. These requirements are a slightly simpli ed model of a failure-free crossroad. For example, we do not model roads with either priority or \turn left" lanes.

2.2 Tra c light requirements

Figure 3 summarizes the requirements for a tra c light. It has three lamps of three di erent colors. Each lamp can be in three di erent states: on, o or ashing. The conjunction of the lamp states characterizes the light state. Whereas generally a single lamp is switched on or ashing at a given time, in the English lights red and yellow can be on at the same time. For ergonomical reasons not all lamp state conjunctions are used. For example, in the three di erent kinds of lights that we consider, green is never on at the same time as other lamps. The light operation is speci ed by a cycle of light states. For example, the German light cycle is red ! yellow ! green ! yellow ! red ; the French light cycle is red ! green ! yellow ! red ; and the English cycle is red ! yellow-and-red ! green ! yellow ! red. The semantics of a light is given by a convention which tells how to interpret each light state. For example, green is known to mean that vehicles can cross, while red means that they are not allowed to. Note that the interpretation is possibly depending on the place of the color in the cycle. For example, yellow in Germany means either that the vehicles have to clear the crossroad if the light was previously green, or that they will soon be able to cross 1. The crossroad is composed of a number of roads which cross each other. 2. The crossroad can be regulated.

Availability Safety

3. At least one road can cross. 4. No more than one road can cross at a given time. 5. Before switching from one crossing road to another, the crossroad must be clear of vehicles. 6. Each road can cross in turn. Figure 2: Intrinsic properties of a crossroad

Fairness

PI n 1424

6 1. 2. 3. 4. 5.

Ducasse & Roze

Three lamps of three di erent colors can be switched on, o or ashing. The light state is characterized by the conjunction of the lamp states. For ergonomical reasons not all the lamp state conjunctions are used. The light operation is speci ed by a cycle of light states. The semantics is given by an interpretation of each state (possibly depending of its place in the cycle). 6. A tra c light is initialized in a state which means that the crossroad is not regulated. Figure 3: Tra c light requirements

if the light was previously red. A tra c light is initialized in a state which means that the crossroad is not regulated. For example, it is initialized at ashing yellow in France, and black (all lamps switched o ) in England.

3 System architecture
Figure 4 gives the global architecture of the speci cation of a crossroad with two tra c lights. Boxes behind other boxes represent re nements of the machines on top of them. Plain lines represent importations of machines, dotted lines represent inclusions of machines. Machine Crossroad models the rights of the vehicles of the roads to cross the crossroad. As there are no criteria to decide which road should start to cross rst, this speci cation is non deterministic. In this machine, there is no mention of lights or colors whatsoever. The machine includes machine Road state which contains a number of constants useful throughout the design. Machine Crossroad2 removes the non-determinism by making an arbitrary choice. Note that it is valuable that the intrinsic \don't care" non-determinism is speci ed at top-level. For example, if a further criterion comes into the design and gives a good reason to make another choice, it will be straightforward to modify the re nement with no need to rethink the speci cation. Machine Crossroad3 is the implementation of Crossroad. It imports machine Light monitor which monitors the tra c lights of the crossroad. Machine Light monitor models the state automaton of the tra c lights. Machine Light monitor2 is a data re nement of Light monitor. It introduces the fact that the states of the automaton are represented by colors without going into the details of which color codes which states. Machine German Light monitor does code precisely the cycle of colors for the German lights. At this point, changing only one constant would enable to implement either French or English lights instead of the German ones. Moreover, this is the only place in the overall design where something has to be changed in order to accommodate a di erent cycle of colors (see

Irisa

\Tra c lights" B case study

7

Crossroad3
Implementation

German_Light_monitor A.light_color2
Implementation Implementation

A.gg.Lamp
Green lamp of light of road A

A.light_color Crossroad2
Reduction of non?determinsim

Light_monitor2 Imports
Data refinement Ring of colors

A.yy.Lamp
Yellow lamp of light of road A

Traffic light colors for road A

Crossroad
Ring of crossing rights

Light_monitor
States of automaton

A.rr.Lamp Imports B.light_color2
Implementation Red lamp of light of road A

B.light_color Includes Includes Road_state
Constants Traffic light colors for road B

B.gg.Lamp
Green lamp of light of road B

B.yy.Lamp
Yellow lamp of light of road B

Light_state
States of lights

B.rr.Lamp
Red lamp of light of road B

Figure 4: Global architecture

PI n 1424

8

Ducasse & Roze

section 4.11 for more details). Machine German Light imports Light state and two instances of the Light color machine, one for each road. Machine Light state is a basic machine which encapsulates a single variable to handle the state of the light monitor automaton. Machine Light color models the colors of the tra c lights of a given road. As our system models two roads we need two instances of this machine. Machine Light color2 implements Light color. It imports three instances of machine Lamp. Machine Lamp models a physical lamp of a tra c light. The implementations of the three basic machines Road state, Light state and Lamp are straightforward, they are therefore not detailed in the following.

4 Abstract machines
In this section we give the B source for all the machines. Section 4.1 describes the design principles of the crossroad machines. Section 4.2 lists the constants de ned in the Road states machine. Section 4.3 presents the Crossroad abstract machine and Section 4.4 its rst re nement. Before describing the implementation of Crossroad (Section 4.7), we present the principles and speci cation of Light monitor the imported machine in Sections 4.5 and 4.6. The re nement of Light monitor is given in Section 4.8. Before describing the implementation of Light monitor (Section 4.11), we present the speci cation of Light state and Light color the imported machines in Sections 4.9 and 4.10. Before describing the implementation of Light color (Section 4.13) we present Lamp, its imported machine in Section 4.12.

In order to encode the previous requirements we use three notions: crossing right, transitional phase, cycle of road states. They are as follows. Crossing right: It models for a given road whether its vehicles are allowed to cross the crossroad or not. This notion is important to take into account most properties of Figure 2: at least one road has the right to cross (prop. 3), only one road has the right to cross (prop. 4) and each road has the right to cross in turn (prop. 6). We use cross to model the fact that a road is allowed to cross and stop to model the fact that a road is not allowed to cross. Transitional phase: Before switching the crossing rights, property 5 of Figure 2 states that the crossroad must be clear of vehicles. The transitional phase models the fact that the vehicles in the middle of the crossroad need time to clear it. We use cross end to model the fact that a road has to clear the crossroad and stop end to model the fact that a road will soon be allowed to cross. Cycle of road states: For a given road the cycle of road states is modeled into a function called following. It is: cross ! cross end ! stop ! stop end ! cross .

4.1.1 States of a given road:

4.1 Crossroad design principles

Irisa

\Tra c lights" B case study

9

The state of a road can be deduced from the other one. For example, if road A can cross, road B is necessarily stopped. Therefore we de ne a function opposite state: opposite state = f(cross 7! stop ) (stop 7! cross ) (cross end 7! stop end ) (stop end 7! cross end )g and deduce the state of road B by roadB state= opposite state(roadA state).
; ; ;

4.1.2 States of the other road:

If the cycle of crossing rights for road A is cross ! cross end ! stop ! stop end ! cross , by de nition of opposite state and of roadB state, the cycle of the couples (RoadA state, RoadB state), which represents the cycle of the crossroad states, will necessarily be: (cross, stop) ! (cross end, stop end) ! (stop, cross) ! (stop end, cross end). It is then the case that: at least one road can cross. Indeed, for all the possible states there is always one of the roads in either cross or cross end states (property 3.) No more than one road can cross at a given time. Indeed, in all the possible states no more than one road is either cross or cross end (property 4.) Before switching from one crossing road to another, the crossroad must be clear of vehicles. Indeed, in the cycle of crossroad states, the two roads are systematically both in a transitional state before any switch of crossing rights. Provided that the transitional phase is reasonably long and that the tra c ows freely enough, the crossroad will be cleared before the new road does cross (property 5.) Each road can cross in turn. Indeed, in the cycle of crossroad states, all four states appear for each road and, hence, each road can cross (property 6.) In summary, with this design, provided that the transitional phases give the opportunity to clear the crossroad, if the cycle of states for road A is as speci ed earlier then the properties of availability, safety and fairness of Figure 2 hold. In the crossroad abstract machine we thus only have to prove, that when regulating the crossroad, following (the function modeling the cycle of road A states) satis es: following(cross) = cross end ^ following(cross end) = stop ^ following(stop) = stop end ^ following(stop end) = cross and that the two road states satisfy: roadB state= opposite state(roadA state). The Road state machine (see Figure 5) has been introduced to encapsulate the constants and sets used in the Crossroad and Light monitor machines. It de nes the set of crossing rights as introduced in the previous section. The o state means that the road is not regulated

4.1.3 Requirements taken into account:

4.2 The Road state machine

PI n 1424

10

Ducasse & Roze

MACHINE Road state SETS CONSTANTS
opposite state

STATE = fcross, cross end, stop, stop end, o

g

PROPERTIES END

opposite state 2 STATE STATE ^ opposite state = fcross 7! stop, cross end 7! stop end, stop 7! cross, stop end 7! cross end , o

7!

o

g

Figure 5: De nitions of sets and constants included in many machines

(neither by a policeman, nor by tra c lights). The constant, opposite state, is used to deduce the state of a road from the state of the other one. It is as introduced in the previous section, except that we have added o 7! o to take into account the \non-regulated" state. Figure 6 gives the speci cation of Crossroad. It uses two constants: following and opposite state. Constant following models the crossing right cycle. It is an abstract constant: it will be re ned in Crossroad3. Constant opposite state is de ned in the included Road state machine. The properties ensure that the requirements of the crossroad are ful lled, as discussed in section 4.1. Three variables are su cient to model the crossroad : global state, roadA state and roadB state. Variable global state models whether the crossroad is regulated or not. Variables roadA state and roadB state model the roads (called roadA and roadB). They must be consistent with each other as stated by the INVARIANT clause. The global property of the crossroad is, of course, strongly correlated to the states of the roads. This is expressed in the last part of the invariant. Indeed, if the crossroad is not regulated the roads are o , and conversely if the roads are o the crossroad is not regulated. Initially, the crossroad is supposed not to be regulated. Two operations are introduced : start up and road state change. Operation start up is used to switch on the regulation of the crossroad. The precondition is that the crossroad must be not regulated. The operation consists of two substitutions: the rst one makes the crossroad regulated and the other one assign a road state to both roadA state and roadB state. This operation is intrinsically non deterministic: with which states of the crossing right cycle roadA and roadB start is irrelevant, provided that these states are elements of STATE - o and that roadB state is the opposite state of roadA state.

4.3 The Crossroad speci cation machine

Irisa

\Tra c lights" B case study

11

MACHINE Crossroad INCLUDES Road state ABSTRACT CONSTANTS SETS
following

PROPERTIES VARIABLES

CSTATE=fregulated, not regulatedg following 2 STATE STATE ^ following(cross) = cross end ^ following(cross end) = stop ^ following(stop) = stop end ^ following(stop end) = cross ^ following(o ) = o

INVARIANT

global state, roadA state, roadB state global state 2 CSTATE ^ roadA state 2 STATE ^ roadB state 2 STATE ^ roadB state = opposite state(roadA state) ^ ((global state = not regulated) , (roadA state = o )) global state := not regulated
jj

INITIALISATION

OPERATIONS start up = PRE global state = not regulated THEN global state := regulated jj ANY aa WHERE aa 2 STATE - fo g THEN roadA state := aa jj roadB state := opposite state(aa) END END ; road state change = PRE global state = regulated THEN roadA state := following(roadA state) jj roadB state := following(roadB state) END END
PI n 1424

roadA state := o

jj

roadB state := o

Figure 6: Speci cation of the Crossroad abstract machine

12

Ducasse & Roze

Operation road state change is used to change the state of the roads. The precondition imposes that global state is regulated. The operation contains two substitutions in order to update the state of both roadA and roadB. In the rst re nement, Crossroad2 (see Figure 7), we reduce the non determinism: we arbitrarily decide that roadA is the one which starts to cross and roadB is the one which starts to stop. As stated in the invariant of crossroad, the global state of crossroad is entirely determined by the value of roadA state. This variable was important to specify but it does not need to be implemented. Variable roadB state is also entirely determined by the value of roadA state, but in this case we do need to implement it to give orders to the tra c light of road B. We therefore keep two variables roadA state2 and roadB state2. As there is no data re nement, they are respectively equal to roadA state and roadB state1 . In the operation start up the non deterministic substitution ANY is replaced by two substitutions: roadA state := and roadB state := . Note that the preconditions do not need to be repeated.
cross stop

4.4 The Crossroad rst re nement

The last Crossroad machine is the implementation. It imports the Light monitor machine. We therefore rst explain the light monitor design principles. We want to be able to implement either French, German or English lights. We have already explained that the three cycles of colors are di erent. We therefore need to handle an abstraction of this cycle. Light automaton. A tra c light is actually nothing but an automaton with 5 states. The initial state corresponds to the crossroad not being regulated. Four states represent the regulated operations and form a cycle: s1 ! s2 ! s3 ! s4 ! s1. This cycle is modeled by a bijection called next where, in addition, next(s0) is s0. Convention. Drivers need to know how to interpret these states. We therefore introduce a bijection, named convention which can be for example: f(o , s0), (cross, s1), (cross end, s2), (stop, s3), (stop end, s4)g. Color association. Then we only need to associate a light color to each state. Road state Light states French color German color English color o s0 ashing yellow ashing yellow black cross s1 green green green s2 yellow yellow yellow cross end stop s3 red red red stop end s4 red yellow yellow and red Note that only the English lights could avoid to use the light state variable as there is a bijection between the states and colors. For the French and German lights, one color is
1 In the atelier, it is not necessary to repeat the variables in that case. For pedagogical purposes we show the verbose form, easier for beginners.

4.5 Tra c light monitor design principles

Irisa

\Tra c lights" B case study

13

REFINEMENT Crossroad2 REFINES Crossroad INCLUDES Road state ABSTRACT CONSTANTS VARIABLES
following

INVARIANT

roadA state2, roadB state2

INITIALISATION
roadA state2 := o

roadA state2 = roadA state ^ roadB state2 = roadB state
jj

OPERATIONS start up = BEGIN roadA state2 := cross END ; road state change = BEGIN

roadB state2 := o

jj

roadB state2 := stop

END END

roadA state2 :=following(roadA state2) roadB state2 :=following(roadB state2)

jj

Figure 7: First re nement of the Crossroad abstract machine

PI n 1424

14

Ducasse & Roze

associated with two states (red for the French light and yellow for the German one). For these colors, in order to determine the next color one needs to know in which state the light is. In order for the design to be general, the light states are thus necessary. The cycle of crossroad states is then implemented by convention and next, namely: following = convention ; next ; convention?1 . Figure 8 gives the speci cation of the Light monitor abstract machine. Set LIGHT STATE is the set of states of the light automaton. The two constants, convention and next, are as described earlier. The light monitor has two variables: lightA state and lightB state. They represent the state of the light automaton of each road. The state of the light automaton of roadB must be consistent with lightA state as shown in the INVARIANT clause. Initially, the lights do not regulate the crossroad. Two operations specify the behavior of the light automaton: start up and light change. They are very similar to the operations of crossroad. The main di erence is that start up has one parameter (crossright) which corresponds to the initial state of the road.

4.6 The Light monitor speci cation machine

4.7 The Crossroad implementation

Figure 9 gives the implementation of the Crossroad abstract machine. An instance of Light monitor, called lm, is imported. Thanks to the invariant of Light monitor, lightB state can be deduced from lightA state. Therefore the INVARIANT of the crossroad implementation only has to specify the links between roadA state and lightA state. Abstract constant following is re ned with the two constants next and convention introduced in Light monitor. The operations are implemented by simply calling the corresponding operations of light monitor.

Figure 10 gives the rst re nement of the Light monitor abstract machine. The drivers are not interested in the light automaton but in the colors of the lights. The aim of Light monitor2 is to introduce these colors in a generic way. Generic means that the machine still models French, German and English tra c lights. The set COLOR represents all the possible colors of a light. Black means that no lamps are switched on; red-yellow means that both the yellow and red lamps are switched on. Each state of the light automaton is associated to a single color. This association is introduced by constant color which is a total function from LIGHT STATE to COLOR. In this machine we do not know which color encodes which state: we just know that each state is coded by a di erent color. This makes the re nement generic. The data re nement introduces variables colorA2 and colorB2 which are the color associated to the states of the light monitor. As discussed in section 4.5 colors alone are not su cient to model the German lights. Therefore variables light state are still necessary,

4.8 The Light monitor rst re nement

Irisa

\Tra c lights" B case study

15

MACHINE Light monitor INCLUDES Road state SETS CONSTANTS PROPERTIES
convention, next

LIGHT STATE = fs0, s1, s2, s3, s4g ;

VARIABLES

convention 2 STATE LIGHT STATE ^ next 2 LIGHT STATE LIGHT STATE ^ convention = fcross 7! s1, cross end 7! s2, stop 7! s3, stop end 7! s4, o next = fs1 7! s2, s2 7! s3, s3 7! s4, s4 7! s1, s0 7! s0g lightA state, lightB state lightA state 2 LIGHT STATE ^ lightB state 2 LIGHT STATE ^ lightB state = convention(opposite state(convention?1 (lightA state))) lightA state := convention(o )
jj

7!

s0g ^

INVARIANT

INITIALISATION

PRE : (lightA state = convention(o )) THEN lightA state := next(lightA state) jj END END

lightA state := convention(crossright) jj lightB state := convention(opposite state(crossright)) END ; light change = lightB state := next(lightB state)

OPERATIONS start up(crossright) = PRE crossright 2 STATE - fo THEN

lightB state := convention(o )

g^

lightA state = convention(o )

Figure 8: Speci cation of the Light monitor abstract machine

PI n 1424

16

Ducasse & Roze

IMPLEMENTATION Crossroad3 REFINES Crossroad2 IMPORTS lm.Light monitor PROPERTIES INVARIANT OPERATIONS start up = BEGIN lm.start up(cross) END ; road state change = BEGIN lm.light change END END

following = (convention ; (next ; convention?1 )) lm.lightA state = convention(roadA state2)

Figure 9: Implementation of the Crossroad abstract machine

Irisa

\Tra c lights" B case study

17

REFINEMENT Light monitor2 REFINES Light monitor INCLUDES Road state CONSTANTS SETS
color

PROPERTIES VARIABLES INVARIANT

COLOR = fgreen, yellow, red, ashing yellow, black, red yellowg color 2 LIGHT STATE ! COLOR

lightA state2, colorA2, lightB state2, colorB2

INITIALISATION

lightA state2 = lightA state ^ colorA2 2 COLOR ^ colorA2 = color(lightA state) ^ lightB state2 = lightB state ^ colorB2 2 COLOR ^ colorB2 = color(lightB state) colorA2 := color(convention(o lightA state2 := convention(o colorB2 := color(convention(o lightB state2 := convention(o

colorA2 := color(convention(crossright)) jj lightA state2 := convention(crossright)jj colorB2 := color(convention(opposite state(crossright))) jj lightB state2 := convention(opposite state(crossright)) END ; light change =

OPERATIONS start up(crossright) = BEGIN

)) ) )) )

jj jj jj

BEGIN

END END

lightA state2 := next(lightA state2) jj colorA2 := color(next(lightA state2)) jj lightB state2 := next(lightB state2) jj colorB2 := color(next(lightB state2))

PI n 1424

Figure 10: First re nement of the Light monitor abstract machine

18

Ducasse & Roze

MACHINE Light state SETS VARIABLES
state

LIGHT STATE = fs0, s1, s2, s3, s4g

INVARIANT
state := s0

INITIALISATION

state 2 LIGHT STATE

OPERATIONS set(val) = PRE val 2 LIGHT STATE THEN state := val END ; res value = BEGIN res := state END END
Figure 11: The Light state basic machine hence lightA state2 and lightB state2. The last part of the invariant expresses the strong correlation between variables color and light state. Figure 11 gives the Light state basic machine which encapsulates a simple variable. It contains a set (LIGHT STATE) of ve elements, a variable state which is in LIGHT STATE and two operations set and value. Operation set is used to give a value to the variable state; operation value is used to return the value of state. The Light color machine (see Figure 12) is an abstraction of the physical light. It contains a set (COLOR), a variable (color) which is in COLOR, and an operation to set the value of

4.9 The Light state basic machine

4.10 The Light color speci cation machine

Irisa

\Tra c lights" B case study

19

MACHINE Light color SETS VARIABLES
color

COLOR = fgreen, yellow, red, ashing yellow, black, red yellowg

INVARIANT

INITIALISATION OPERATIONS set(val) = PRE val 2 COLOR THEN color := val END; END
color := black

color 2 COLOR

Figure 12: The Light color abstract machine

the variable. It would be straightforward to add an operation to get the value, but we do not need it in the current design. An example of light monitor implementation is given by Figure 13. It implements the German light monitor. It imports two instances of machine Light color: cA and cB which are the lights for roadA and roadB respectively. It also imports an instance ls of machine Light state to handle the state of the light automaton. The invariant links the color of cA (cB) and the state of roadA state (roadB state) with respectively the color colorA2 (colorB2) and the state lightA state2 (lightB state2) of its abstraction, Light monitor2. The initialization and the operations are identical to those of light monitor2 but are implemented with the operations of the machines Light state and Light color. It should be stressed that in oder to make an implementation for another country only the color constant has to be changed. For English lights: =f1! 2! 0 ! g. For French lights: = f1 ! 3! 4 ! 2! 3! 4! 0! g
color s green; s s yellow; s red; s red yellow; s black color yellow; s red; s red; s f lashing yellow

4.11 The German Light monitor implementation

green; s

PI n 1424

20

Ducasse & Roze

IMPLEMENTATION German Light monitor REFINES Light monitor2 INCLUDES Road states IMPORTS cA.Light color, cB.Light color, ls.Light state VALUES INVARIANT

convention= fcross 7! s1, cross end 7! s2, stop 7! s3, stop end 7! s4, o 7! s0g ; next = fs1 7! s2, s2 7! s3, s3 7! s4, s4 7! s1, s0 7! s0g ; color=fs1 7! green, s2 7! yellow, s3 7! red, s4 7! yellow, s0 7! ashing yellowg colorA2 = cA.color ^ lightA state2 = ls.state ^ colorB2 = cB.color ^ lightB state2 = convention(opposite state(convention?1 (ls.state)))

INITIALISATION cA.set(color(convention(o ))); cB.set(color(convention(o ))); ls.set(convention(o )) OPERATIONS start up(crossright) = BEGIN cA.set(color(convention(crossright))); cB.set(color(convention(opposite state(crossright)))); ls.set(convention(crossright)) END ; light change = BEGIN VAR lsstate IN lsstate ls.value; ls.set(next(lsstate)) ; cA.set(color(next(lsstate))) ; cB.set(color(next(convention(opposite state(convention ?1(lsstate)))))) END END END
Figure 13: Implementation of the German light abstract machine

Irisa

\Tra c lights" B case study

21

MACHINE Lamp SETS VARIABLES
lam

LAMP STATE = flon, lo , ashingg

INVARIANT
lam := lo

INITIALISATION

lam 2 LAMP STATE

OPERATIONS set(st)= PRE st 2 LAMP STATE THEN lam := st END END

Figure 14: Speci cation of the lamp abstract machine

COLOR has been built to address these three examples. It could be easily extended to take more colors into account, for example, ashing green if it were of any interest. This modi cation would have to be propagated to Light color and its re nements.

The Lamp machine (see Figure 14) models one lamp of a light by one variable, lam in LAMP STATE. Lamp states lon, lo and ashing respectively mean that the lamp is switched on, switched o and ashing. The set operation switches the lamp to the desired state. The implementation light color2 (see Figure 15) imports three instances of machine Lamp in order to re ne the variable color with the lamps of the light. The invariant expresses the correlation between variable color and the three variable instances of Lamp. Operation set of machine Lamp is used to switch lamps according to the desired color. For example, in order to get the green color, only the green lamp has to be switched on. Thus, (gg.lam,

4.12 The Lamp speci cation machine

4.13 The Light color implementation

PI n 1424

22

Ducasse & Roze

IMPLEMENTATION Light color2 REFINES Light color IMPORTS gg.Lamp, yy.Lamp, rr.Lamp INVARIANT

OPERATIONS set(val) = PRE val 2 COLOR THEN CASE val OF EITHER green THEN rr.set(lo ) ; yy.set(lo ) ; gg.set(lon) OR yellow THEN rr.set(lo ) ; yy.set(lon) ; gg.set(lo ) OR red THEN rr.set(lon) ; yy.set(lo ) ; gg.set(lo ) OR ashing yellow THEN rr.set(lo ) ; yy.set( ashing) ; gg.set(lo ) OR black THEN rr.set(lo ) ; yy.set(lo ) ; gg.set(lo ) OR red yellow THEN rr.set(lon) ; yy.set(lon) ; gg.set(lo ) END END
Figure 15: Implementation of the light color abstract machine

((color=green) ) ((gg.lam=lon) ^ (yy.lam=lo ) ^ (rr.lam=lo ))) ^ ((color=yellow) ) ((gg.lam=lo ) ^ (yy.lam=lon) ^ (rr.lam=lo ))) ^ ((color=red) ) ((gg.lam=lo ) ^ (yy.lam=lo ) ^ (rr.lam=lon))) ^ ((color=black) ) ((gg.lam=lo ) ^ (yy.lam=lo ) ^ (rr.lam=lo ))) ^ ((color=red yellow) ) ((gg.lam=lo ) ^ (yy.lam=lon) ^ (rr.lam=lon))) ^ ((color= ashing yellow) ) ((gg.lam=lo ) ^ (yy.lam= ashing) ^ (rr.lam=lo )))

yy.lam, rr.lam) have to be substituted by (lon, lo , lo ). This is achieved by gg.set(lon) ; yy.set(lo ) ; rr.set(lo ).

5 Conclusion
We have presented a totally revised version of the crossroad abstract machine of Chauvet. It illustrates re nement invariants, data re nement, reduction of non-determinism and importation. It is also exible enough to accommodate the di erent light automata of France, England and Germany by changing a single constant. The case study is used in a B course. It has been implemented and proved in the B atelier. It has been integrated in an operational simulator.

Irisa

\Tra c lights" B case study

23

Acknowledgments We are indebted to Philippe Ingels for his signi cant help to design
the abstract machines and prove them correct with the B atelier.

References
1] J.-R. Abrial. The B Book: Assigning programs to meanings. Cambridge University Press, 1996. 2] J.-Y. Chauvet. Une etude de cas en B : les feux tricolores. In Habrias, ed, 1st conference on the B Method, pages 329{351, Univ. de Nantes, France, Nov. 1996. 3] M. Ducasse. Teaching B at a technical university is possible and rewarding. In Habrias and Dunn, eds, B'98, Proc. of the Educational Session. april 1998. 4] Steria Mediterranee. Atelier b. http://www.atelierb.societe.com/. 5] C. Morgan. Programming from speci cations, 2nd edition. International Series in Computer Science. Prentice Hall, 1994. ISBN 0-13-123274-6. 6] E. Sekerinski and K. Sere, editors. Program development by re nement, Case studies using the B method. Formal Approaches to Computing and Information Technology. Springer, 1999.

PI n 1424

24

Ducasse & Roze

1 Introduction 2 Requirements

Contents

2.1 Crossroad requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Tra c light requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3 4
4 5

3 System architecture 4 Abstract machines

4.1 Crossroad design principles . . . . . . . . . 4.1.1 States of a given road: . . . . . . . . 4.1.2 States of the other road: . . . . . . . 4.1.3 Requirements taken into account: . . 4.2 The Road state machine . . . . . . . . . . . 4.3 The Crossroad speci cation machine . . . . 4.4 The Crossroad rst re nement . . . . . . . . 4.5 Tra c light monitor design principles . . . 4.6 The Light monitor speci cation machine . . 4.7 The Crossroad implementation . . . . . . . 4.8 The Light monitor rst re nement . . . . . 4.9 The Light state basic machine . . . . . . . . 4.10 The Light color speci cation machine . . . . 4.11 The German Light monitor implementation 4.12 The Lamp speci cation machine . . . . . . . 4.13 The Light color implementation . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . .

8 8 9 9 9 10 12 12 14 14 14 18 18 19 21 21

6 8

5 Conclusion

22

Irisa


更多相关文档:

The traffic lights are the same in every country.doc

traffic| The traffic lights are the same in every country_管理学_高等教育_教育专区。The traffic lights are the same in every country . There are ...

DESIGN THE SWITCHING PERIOD FOR TRAFFIC LIGHT.doc

DESIGN THE SWITCHING PERIOD FOR TRAFFIC LIGHT_英语考试_外语学习_教育专区。美... so in the case of one-hour period, there are 360 periods, the ranges...

二年级下册英语课件-Unit 4 Lesson 20 Traffic Lights冀教版 (....ppt

河北教育出版社 二年级 | 下册 Unit 4 Lesson 20 Traffic lights 河北教育出版社 二年级 | 下册 Warm-up wait 河北教育出版社 二年级 | 下册 traffic 河北...

最新人教新版英语三上《How were traffic lights born》教学设计_....doc

traffic lights D.cars A. people ( )5、The ____________ lights stop the cars. B.red C.green D.yellow A.traffic ----------优秀教案资料-...

三年级英语上册 How were traffic lights born教案 人教新版.doc

shops C. traffic lights D.cars ()5、The ____________ lights stop the cars. A.traffic B.red C.green D.yellow 此资源为 word 格式,您下载后...

traffic lights_图文.ppt

traffic lights_育儿知识_幼儿教育_教育专区。road traffic lights √ × zebra crossing stop across road traffic lights √ × zebra crossing stop across ...

三年级英语上册 How were traffic lights born教案 人教新版完美....doc

问题: ()1、Traffic lights are very ____________ to us. A. important B.new C.old D.poor ()2、Gerret.A.Morgan was the ____________...

trafficlights教案.doc

blackboard design: teaching reflection: 【篇二:小学英语教师资格面试《traffic lights》教案】 2016 下半年教师资格面试备考已经拉开序幕,一篇优秀的教案对面 试的...

小学英语教师资格面试《Traffic+lights》教案.doc

小学英语教师资格面试《Traffic+lights》教案_英语_小学教育_教育专区。小学英语教师资格面试《Traffic lights》教案 Traffic lights teaching plan Teaching Aims: ...

7.Significant Of Traffic Light Control System.doc

Significant Of Traffic Light Control System The traffic lights are also known as stoplights, traffic signals, road traffic lamps, that is a signalling ...

pep英语traffic lights.ppt

pep英语traffic lights_六年级英语_英语_小学教育_教育专区。Look at the ...B: You can go by the No.15 bus. A: Can I go on foot? B: Sure,...

traffic lights.ppt

B: Sure, if you like .It’s not far. Please make another dialogue with your partner. Let’s read The traffic lights are the same in every country...

代理控制交通灯(AgentControlledTrafficLights)毕业论文外文文献....doc

代理控制交通灯(AgentControlledTrafficLights)毕业论

Wait for the traffic lights to change._图文.ppt

Wait for the traffic lights to change._初

traffic light on stm32.doc

7 Yingtong Guo Tianyi Miao Mini-Project Traffic Light Systems Appendix A #...{ GPIO_InitTypeDef GPIO_InitStructure; //initialized GPIO A,B,C //...

...caution traffic lights could prevent accidents: study_论文....pdf

Length of yellow caution traffic lights could prevent accidents: study_英语考试_外语学习_教育专区。2013年第2期 t 悦读 Reach f0i new heigl’健 考试? 新...

...turning()the left after the traffic lights. _答....doc

It's the first turning()the left after the traffic lights. A. on B. in C. by D. for_答案解析_2016年_一模/二模/三模/联考_图文_百度高考

DesignOfTrafficLight.pdf

DesignOfTrafficLight_信息与通信_工程科技_专业资料。Design Of Traffic Light ...CPSC 5155 Chapter 7 Slide 6 of 17 slides Step 1b: Define the State ...

Wait for the traffic lights to change._图文.ppt

Wait for the traffic lights to change._学科竞赛_高中教育_教育专区。 单元主题写作三 常用表达 1.Drivers and pedestrians must the traffic rules. 2.Mind ...

小学英语教师资格面试《Traffic lights》教案.doc

小学英语教师资格面试《Traffic lights》教案 2017 下半年教师资

更多相关标签:
网站地图

文档资料共享网 nexoncn.com copyright ©right 2010-2020。
文档资料共享网内容来自网络,如有侵犯请联系客服。email:zhit325@126.com