Dines Bjørner From Domains to Requirements

(1)

From Domains to Requirements

A Gentle Introduction to Domain Engineering

1

July 5, 2013: 14:26

(2)

(3)

Dines Bjørner Fredsvej 11 DK–2840 Holte Denmark bjorner@gmail.com www.imm.dtu.dk/˜dibj

• Assembly and writing of these lecture notes was begun on June 3, 2013.

• They are composed primarily from either published or draft papers.

• These lecture notes are paired with a set of lecture slides.

• At present, July 5, 2013, the lecture notes comprise??pages and 650 slides.

• Margin-numbers in these lecture notes refer to slide numbers.

c

Dines Bjørner, 2013

(4)

(5)

to Kari Skallerud Bjørner

(6)

(7)

In 2006 I published the 3 volume, approximately 2400 page, bookSoftware Engineeringι1–ι3. In 2009 Qinhua University Press, in agreement with Springer Verlag, republished these books, in Englishι4–ι6, then in Chineseι7–ι9.

In the years between 2006 and now I have lectured over these books and also rewritten major parts ι10–ι13. I spent the year Feb. 2006–Jan. 2007 inclusive at JAIST^∗. I used ι1–ι3 as the basis for my lectures there. A group of Chinese PhD students, led by (now) Dr. Liu BoChao, proposed to translate the three volumes into Chinese. Dr. Liu completed this task – for which I owe him innumerable thanks.

Around New Year 2008/2009 Prof. Kokichi Futatsugi, my host at JAIST, kindly asked me to edit my mostly technical reports written during my stay at JAIST in a form suitable for publication. That became [14].

There was one area of the Software Engineering which I have continued to research. It is that of Domain Engineering ι15–ι25 in particular Domain Analysis. In addition to the above ten 2008–

2013 publications I have experimentally developed a number of (unpublished) domain descriptions: for container lines ι26,pipe lines ι27–ι28,financial services (stock exchanges)ι29,[road] transportation systems ι30 anddocuments ι31 — to mention some.

During the spring and summer of 2013 I started on a series of domain science and engineering- related documents. First ι32, then the invited paperι25 in which a summary of the domain analysis parts ofι32 forms a basis. That lead me to envisage a series of papers, all with an extract ofι32 as the basis:ι33–ι37. Chapter 2 of this book is based onι32. Chapter 3 on the second part ofι33. Chapter 4 on the second parts ofι25 andι35. Chapter 5 on the second part ofι36. Chapter 7 is based onι16.

Other chapters of this book are new. The writing ofι32–ι37 amounts to also completing this book.

I hope to be able to publishι32–ι37, once sufficiently polished, during the next year while likewise hopefully using this book as a basis for PhD lectures around Europe.

ι1–ι9,ι14

∗JAIST: Japan Advanced Institute of Science and Technology, Ishikawa Province, near Kanazawa, Japan

(8)

References

ι1. Software Engineering, Vol. 1: Abstraction and Modelling. Texts in Theoretical Computer Sci- ence, the EATCS Series. Springer, 2006. . ι2. Software Engineering, Vol. 2: Speciﬁcation of Sys-

tems and Languages. Texts in Theoretical Com- puter Science, the EATCS Series. Springer, 2006.

Chapters 12–14 are primarily authored by Chris- tian Krog Madsen.

ι3. Software Engineering, Vol. 3: Domains, Require- ments and Software Design. Texts in Theoretical Computer Science, the EATCS Series. Springer, 2006.

ι4. Software Engineering, Vol. 1: Abstraction and Modelling. Qinghua University Press, 2008.

ι5. Software Engineering, Vol. 2: Speciﬁcation of Sys- tems and Languages. Qinghua University Press, 2008.

ι6. Software Engineering, Vol. 3: Domains, Require- ments and Software Design. Qinghua University Press, 2008.

ι7. Chinese: Software Engineering, Vol. 1: Abstrac- tion and Modelling. Qinghua University Press.

Translated by Dr Liu Bo Chao et al., 2010.

ι8. Chinese:Software Engineering, Vol. 2: Speciﬁca- tion of Systems and Languages. Qinghua Univer- sity Press. Translated by Dr Liu Bo Chao et al., 2010.

ι9. Chinese:Software Engineering, Vol. 3: Domains, Requirements and Software Design. Qinghua Uni- versity Press. Translated by Dr Liu Bo Chao et al., 2010.

ι10. Software Engineering: A Triptych Approach. In- ternet, Summer 2008. 610 pages. [Slightly incomplete draft version.: www.imm.dtu.dk/˜db/- tseb.pdf].

ι11. Domain Engineering. Internet, Summer 2008.

469 pages. [Slightly incomplete draft version.:

www.imm.dtu.dk/˜db/de-p.pdf].

ι12. From Domains to Requirements: The Triptych Ap- proach to Software Engineering. Internet, Sum- mer 2009. Slightly incomplete draft version, approximately XXVII+160+25 pages (frontmatter, main text, appendices). [Click!: www.imm.dtu.- dk/˜db/de+re-p.pdf].

ι13. From Domains to Requirements: The Triptych Ap- proach. Internet, April 2010. Lecture notes cover the first 150 pages of this 342 page compendium.

[Slightly incomplete draft version: www.comp- lang.tuwien.ac.at/bjorner/book.pdf]. [See also long version of [15]: www.imm.dtu.dk/˜db/- from-domains-to-requirements.pdf] (includes for- mulas).

ι14. Domain Engineering: Technology Management, Research and Engineering. Research Monograph (# 4); JAIST Press, 1-1, Asahidai, Nomi, Ishikawa 923-1292 Japan, March 2009. This Research Monograph contains the following main chapters:

(a) On Domains and On Domain Engineering – Prerequisites for Trustworthy Software – A Necessity for Believable Management, pages 3–38.

(b) Possible Collaborative Domain Projects – A Management Brief, pages 39–56.

(c) The Rˆole of Domain Engineering in Software Development, pages 57–72.

(d) Veriﬁed Software for Ubiquitous Computing – A VSTTE Ubiquitous Computing Project Proposal, pages 73–106.

(e) The Triptych Process Model – Process As- sessment and Improvement, pages 107–138.

(f) Domains and Problem Frames – The Triptych Dogma and M.A.Jackson’s PF Paradigm, pages 139–175.

(g) Documents – A Rough Sketch Domain Anal- ysis, pages 179–200.

(h) Public Government – A Rough Sketch Do- main Analysis, pages 201–222.

(i) Towards a Model of IT Security — – The ISO Information Security Code of Practice – An Incomplete Rough Sketch Analysis, pages 223–282.

(j) Towards a Family of Script Languages – – Licenses and Contracts – An Incomplete Sketch, pages 283–328.

ι15. Domain Theory: Practice and Theories, Discus- sion of Possible Research Topics. InICTAC’2007, volume 4701 of Lecture Notes in Computer Sci- ence (eds. J.C.P. Woodcock et al.), pages 1–17, Heidelberg, September 2007. Springer.

ι16. From Domains to Requirements. In Montanari

Festschrift, volume 5065 ofLecture Notes in Com- puter Science (eds. Pierpaolo Degano, Rocco De Nicola and Jos´e Meseguer), pages 1–30, Heidel- berg, May 2008. Springer.

ι17. Compositionality: Ontology and Mereology of Do- mains. Some Clarifying Observations in the Con- text of Software Engineering in July 2008, eds.

Martin Steffen, Dennis Dams and Ulrich Han- nemann. In Festschrift for Prof. Willem Paul de Roever Concurrency, Compositionality, and Correctness, volume 5930 of Lecture Notes in Computer Science, pages 22–59, Heidelberg, July 2010. Springer.

ι18. The Role of Domain Engineering in Software De- velopment. Why Current Requirements Engineer- ing Seems Flawed! InPerspectives of Systems In- formatics, volume 5947 ofLecture Notes in Com- puter Science, pages 2–34, Heidelberg, Wednes- day, January 27, 2010. Springer.

ι19. From Domains to Requirements — On a Triptych of Software Development. Research Report, Uni- versity of Edingburgh, November 2009.

ι20. Domain Engineering. In Paul Boca and Jonathan Bowen, editors,Formal Methods: State of the Art

(9)

and New Directions, Eds. Paul Boca and Jonathan Bowen, pages 1–42, London, UK, 2010. Springer.

ι21. Domain Science & Engineering –From Computer Science to The Sciences of Informatics, Part I of II: The Engineering Part. Kibernetika i sistemny analiz, (4):100–116, May 2010.

ι22. Domain Science & Engineering –From Computer Science to The Sciences of Informatics Part II of II:

The Science Part. Kibernetika i sistemny analiz, (2):100–120, May 2011.

ι23. Domains: Their Simulation, Monitoring and Con- trol – A Divertimento of Ideas and Suggestions.

In Rainbow of Computer Science, Festschrift for Hermann Maurer on the Occasion of His 70th An- niversary., Festschrift (eds. C. Calude, G. Rozen- berg and A. Saloma), pages 167–183. Springer, Heidelberg, Germany, January 2011.

ι24. A Rˆole for Mereology in Domain Science and En- gineering. Synthese Library (eds. Claudio Calosi and Pierluigi Graziani). Springer, Amsterdam, The Netherlands, May 2013.

ι25. Domain Analysis: Endurants – An Analysis & De- scription Process Model [Almost final draft] (paper: www.imm.dtu.dk/˜dibj/jaist-da.pdf., slides:

www.imm.dtu.dk/˜dibj/jaist-s.pdf.). Research Report 2013-9, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, May 2013.

ι26. A Container Line Industry Domain. Techn. report, Fredsvej 11, DK-2840 Holte, Denmark, June 2007. [Extensive Draft: www.imm.dtu.dk/˜db/- container-paper.pdf].

ι27. Pipe System Domain Models. Research 2012-2, DTU Informatics, May 2012.

ι28. Pipelines – a Domain Description: www.imm.dtu.- dk/˜dibj/pipe-p.pdf.. Experimental Research Re- port 2013-2, DTU Compute and Fredsvej 11, DK- 2840 Holte, Denmark, Spring 2013.

ι29. The Tokyo Stock Exchange Trading Rules. R&D Experiment, Fredsvej 11, DK-2840 Holte, Den- mark, January, February 2010.

ι30. Road Transportation – a Domain Description:

www.imm.dtu.dk/˜dibj/road-p.pdf.. Experimen- tal Research Report 2013-4, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Spring 2013.

ι31. Documents – a Domain Description: www.imm.- dtu.dk/˜dibj/doc-p.pdf.. Experimental Research Report 2013-3, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Spring 2013.

ι32. Domain Analysis & Description: Endurants (paper: www.imm.dtu.dk/˜dibj/da-p.pdf. slides:

www.imm.dtu.dk/˜dibj/da-s.pdf.). Research Re- port 2013-1, DTU Compute and Fredsvej 11, DK- 2840 Holte, Denmark, April 2013.

ι33. Domain Analysis & Description: Perdu-

rants [Writing to begin Summer 2013] (paper: www.imm.dtu.dk/˜dibj/perd-p.pdf., slides:

www.imm.dtu.dk/˜dibj/perd-s.pdf.). Research Report 2013-7, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Summer/Fall 2013. A first draft of this document might be written late summer of 2013.

ι34. Domain Analysis: Endurants – An Analysis & De- scription Process Model [Almost final draft] (paper: www.imm.dtu.dk/˜dibj/jaist-da.pdf., slides:

www.imm.dtu.dk/˜dibj/jaist-s.pdf.). Research Report 2013-9, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, May 2013.

ι35. Domain Analysis: Endurants – A Model of Prompts [Early, incomplete draft] (paper:

www.imm.dtu.dk/˜dibj/prompts-p.pdf., slides:

www.imm.dtu.dk/˜dibj/prompts-s.pdf.). Re- search Report 2013-10, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, July 2013.

ι36. Domain Analysis & Description: Modelling Facets [Writing to begin Summer 2013] (paper: www.imm.dtu.dk/˜dibj/da-facets-p.pdf., slides: www.imm.dtu.dk/˜dibj/da-facets-s.pdf.).

Research Report 2013-7, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Sum- mer/Fall 2013. A first draft of this document might be written late summer of 2013.

ι37. On Deriving Requirements from Domain Speci- fications [Writing to begin Summer 2013] (paper: www.imm.dtu.dk/˜dibj/da-fac-p.pdf., slides:

www.imm.dtu.dk/˜dibj/da-fac-s.pdf.). Research Report 2013-8, DTU Compute and Fredsvej 11, DK-2840 Holte, Denmark, Summer/Fall 2013. A first draft of this document might be written late summer of 2013.

2

(10)

(11)

Part I Opening

1 Introduction . . . 3

1.1 TheTripTychApproach to Software Engineering . . . 3

1.1.1 Domain Engineering . . . 3

1.1.2 Requirements Engineering. . . 5

1.1.3 Software Design. . . 5

1.2 An Example: Road Transport. . . 5

1.2.1 Endurants . . . 5

Parts. . . 5

Properties. . . 7

Definitions of Auxiliary Functions. . . 11

Some Derived Traffic System Concepts . . . 11

States. . . 15

1.2.2 Perdurants . . . 15

Actions . . . 15

Events . . . 16

Behaviours . . . 17

1.3 Whither Domain Science & Engineering ?. . . 20

Part II Domains 2 Endurants . . . 25

2.1 Introduction. . . 25

2.2 Formal Concept Analysis. . . 25

2.2.1 A Formalisation . . . 25

2.2.2 Types Are Formal Concepts . . . 26

2.2.3 Practicalities. . . 26

2.2.4 Formal Concepts: A Wider Implication. . . 26

2.3 Endurant Entities . . . 26

2.3.1 General . . . 26

2.3.2 Endurants and Perdurants. . . 27

2.3.3 Endurants . . . 27

2.3.4 Atomic and Composite Parts . . . 28

2.3.5 On Observing Part Sorts . . . 29

Types and Sorts. . . 29

On Discovering Part Sorts. . . 29

Part Sort Observer Functions . . . 29

On Discovering Concrete Part Types . . . 31

Forms of Part Types. . . 32

Part Sort and Type Derivation Chains . . . 32

Names of Part Sorts and Types . . . 32

(12)

Opening

(20)

(21)

Introduction

⁵

Usually a ﬁrst major phase of software development is that of requirements engineering. In this book we present a more general approach to software development in which we preﬁx a domain

engineering phase to the requirements engineering phase. ⁶

We shall thus present a number of techniquesandtools that are of interest in “the very early stages” of software development.

Dogma 1 TripTych: Before we can design software we must have a reasonably firm understanding of its requirements; and before we can prescribe requirements we must have a reasonably firm understanding of the domain in which that software and its supporting hardware has to reside . So the “the very early stages” of software development are those in which one obtains a reasonably

ﬁrm understanding of the domain. 7

Definition 1 Domain: By a^′domain^′we shall understand a set of^′entities^′:^′endurant^′s, that is, phenomena that “lasts”, and^′perdurant^′s, that is actions, events and behaviours over endurants, where the focus (of such entities) is on domains created by humans, domains that are components of a ^′societal infrastructure^′, and where, hence, these users interact, more-or-less casually with their domain, and these human users are not expected to excert greater technical skills in their interaction with the domain .

8

Example1 Domains Some example domains are: air traffic, airports, banking, container lines, heath care, manufacturing (e.g., wither of metal working, machining, assembly, etcetera), pipelines, railways, etcetera .

1.1 The TripTych Approach to Software Engineering

⁹

The key words above were ‘domain’, ‘requirements’, and software’. We shall therefore associate with each of these separatephasesof software development. These are:domain engineering,requirements engineering, andsoftware design.

1.1.1 Domain Engineering ¹⁰

Definition 2 Domain Engineering: By ^′domain engineering^′ we shall understand the process of analysing and describing a domain, that is, of determining the range of domain stake-holders, of gatheringandanalysinginformation about the domain, ofdescribingthe domain, oftesting, checking and verifyingthe evolvingdomain description and ofvalidating that description .

11

We shall define the sans serif terms used in the definition above and also in the definition given below for requirements engineering.

(22)

Definition 3 Domain [Requirements] Stake-holder: By ^′domain stake-holder^′ (^′requirements stake-holder^′) we shall understand a person, or a group of persons, “united” somehow in their common interest in, or dependency on the domain (requirements); or an institution, an enterprise, or a group of such, (again) characterised (and, again, loosely) by their common interest in, or dependency on the domain (requirements) .

In this book we shall not exemplify techniques or tools for stake-holder identiﬁcation.

12

Example2 Stake-holders For the domain of banking one can include the following in its sets of stake-holders: bank owners, bank staff, clients, regulators, the press/media, politicians, suppliers, etcetera .

13

Definition 4 Domain Information Gathering: By ^′domain information gathering^′ we shall understand the process, through interviews, questionnaires, document (literature, etc.) reading, etcetera, of acquiring and recording facts about the domain .

In this book we shall not exemplify techniques or tools for domain information gathering.

14

Definition 5 Domain Analysis: By ^′domain information analysis^′ (or just ^′domain analysis^′) we shall understand the process of asking question and, forming concepts about, and postulating properties of the domain .

This book is indeed about techniques and tools for domain analysis.

15

Definition 6 : By a ^′domain description^′ we shall understand a document, both informal and formal, which describes entities endurants: parts and materials and their qualities (properties), and perdurants: actions, events and behaviours of the domain .

This book is indeed about techniques and tools for domain description

16

Definition 7 Testing: By ^′testing^′ [a domain description (or a requirements prescription)] we shall understand the process of subjecting a domain description (or the requirements prescription) to a number of symbolic (or abstract) interpretations¹given case-specific entity values with a view towards obtaining expected answers .

In this book we shall not exemplify techniques or tools for testing domain or requirements descriptions.

17

Definition 8 Checking: By^′checking^′[a domain description (or a requirements prescription)] we shall understand the process of subjecting a domain description (or the requirements prescription) to a number of model checks²given case-specific domain model instantiations with a view towards obtaining expected answers .

In this book we shall not exemplify techniques or tools for checking domain descriptions or requirements prescriptions.

18

Definition 9 Verification: By^′verification^′ [of a domain description (or a requirements prescription)] we shall understand the process of formally proving properties of a domain description (or a requirements prescription) .

In this book we shall not exemplify techniques or tools for verifying domain descriptions (or requirements prescriptions).

19

Definition 10 Validation: By^′validation^′we shall understand the process of checking with domain stake-holders that that which is described (prescribed) by a domain description (or a requirements prescription) is commensurate with their understanding of the domain (or of their requirements to software for that domain .

1 We assume that the concepts of symbolic or abstract interpretations, [35], are known.

2 We assume that the concepts of model checking, [61, 49, 33, 62], is known.

(23)

In this book we shall not exemplify techniques or tools for validating domain descriptions (or requirements prescriptions).

• • •

Chapter 6 summarises the concept of ‘Domain Engineering’.

1.1.2 Requirements Engineering ²⁰

Definition 11 Requirements Engineering: By ^′requirements engineering^′ we shall understand the process of analysing and prescribing the requirements, that is, of determining the range of requirements stake-holders, of gathering and analysing information about the requirements, of describing the requirements, of testing, checking and verifying the evolving requirements prescription with respect to the underlying domain description, and ofvalidating that prescription .

21

We shall only deﬁne therequirementsterm.

Definition 12 Requirements: By ^′requirements^′ we shall understand a condition or capability needed by a stake-holder to solve a problem or achieve an objective .

Chapter 7 outlines our contribution to the concept of ‘Requirements Engineering’. It is that of

“deriving”, not automatically, but systematically, in an “interactive fashion”, with requirements stake-holders, the requirements from the domain description.

1.1.3 Software Design 22

Definition 13 Software Design: By^′software design^′ we shall understand the process of “trans- forming” (refining) the requirements prescription into executable code, that is, of turning abstract data types into concrete, machine-representable data types, of turning function pre- & post- conditions into algorithms, and of implementing behaviours .

In this book we shall not exemplify techniques or tools for software design.

1.2 An Example: Road Transport

²³

This section can be skipped in any reading of this book ! The example of this book serves the following purposes: to, of course, give an example of a domain description sketch, thus to familiarise the reader to concepts of domain analysis, and to show that one can, indeed, obtain a rather comprehensive description of domains that may, at ﬁrst, seem “too big”. The reader may ascertain the structure of this section by consulting the table-of-contents listing.

1.2.1 Endurants 24

Parts Root Sorts

The root domain, ∆, the stepwise unfolding of whose description is to be exempliﬁed, is that of a composite traffic system (1a.) with a road net, (1b.) with a ﬂeet of vehicles and (1c.) of whose individual position on the road net we can speak, that is, monitor. 25

1. We analyse the composite traﬃc system into (a) a composite road net,

(b) a composite ﬂeet (of vehicles), and (c) an atomic monitor.

(24)

type 1. ∆ 1a. N 1b. F 1c. M value

1a. obs N:∆ →N 1b. obs F:∆→F 1c. obs M:∆→M

Sub-domain Sorts and Types ²⁶

2. From the road net we can observe

(a) a composite part,HS, of road (i.e., street) intersections (hubs) and (b) a composite part,LS, of road (i.e., street) segments (links).

type 2. HS, LS value

2a. obs HS: N→HS 2b. obs LS: N→LS

27 We analyse the sub-domains of HSandLS.

3. From the hubs aggregate we decide to observe (a) the concrete type of a set of hubs,

(b) where hubs are considered atomic; and 4. from the links aggregate we decide to observe

(a) the concrete type of a set of links, (b) where links are considered atomic;

28

type

3a. Hs = H-set 4a. Ls = L-set 3b. H

4b. L value

3. obsHs: HS→H-set 4. obsLs: LS→L-set

29

5. From the ﬂeet sub-domain, F, we observe a composite part,VS, of vehicles type

5. VS value

5. obsVS: F →VS

30

6. From the composite sub-domainVSwe observe

(a) the composite partVs, which we concretise as a set of vehicles (b) where vehicles,V, are considered atomic.

(25)

type

6a. Vs = V-set 6b. V

value

6a. obs Vs: VS→V-set

31 The “monitor” is considered atomic. It is an abstraction of the fact that we can speak of the positions of each and every vehicle on the net without assuming that we can indeed pin point these positions by means of, for example, sensors.

Properties ³²

Parts are distinguished by their properties: the types and the values of these. We consider three kinds of properties: unique identiﬁers, mereology and attributes.

Unique Identifications ³³

There is, for any traﬃc system, exactly one composite aggregation, HS, of hubs, exactly one composite aggregation,Hs, of hubs, exactly one composite aggregation,LS, of links, exactly one composite aggregation, Ls, of links, exactly one composite aggregation,VS, of vehicles and exactly one composite aggregation,Vs, of vehicles, Therefore we shall not need to associate unique identiﬁers with any of these.

7. We decide the following:

(a) each hub has a unique hub identiﬁer, (b) each link has a unique link identiﬁer and

(c) each vehicle has a unique vehicle identiﬁer.

type 7a. HI 7b. LI 7c. VI value

7a. uid H: H→HI 7b. uidL: L→LI 7c. uid V: V→VI

Mereology ³⁴

Road Net Mereology

Bymereologywe mean the study, knowledge and practice of understanding parts and part relations.

The mereology of the composite parts of the road net,n:N, is simple: there is one HSpart of n:N; there is oneHspart of the onlyHSpart ofn:N; there is oneLSpart of n:N; and there is one Lspart of the only LSpart of n:N. Therefore we shall not associate any special mereology based on unique identiﬁers which we therefore also decided to not express for these composite parts. 35

8. Each link is connected to exactly two hubs, that is,

(a) from each link we can observe its mereology, that is, the identities of these two distinct hubs,

(b) and these hubs must be of the net of the link;

9. and each hub is connected to zero, one or more links, that is,

(a) from each hub we can observe its mereology, that is, the identities of these links, (b) and these links must be of the net of the hub.

36

(26)

value

8a. mereo L: L→HI-set axiom

8a. ∀l:L^•card mereo L(l)=2, 8b. ∀n:N,l:L,hi:HI^•

8b. l∈obs Ls(obs LS(n))∧hi∈mereo L(l) 8b. ⇒ ∃h:H^•h∈obs Hs(obs HS(n))∧uid H(h)=hi value

9a. mereo H: H→LI-set axiom

9b. ∀n:N,h:H,li:LI^•

9b. h∈obs Hs(obs HS(n))∧li∈mereo H(h) 9b. ⇒ ∃l:L^•l∈obs Ls(obs LS(n))∧uid L(l)=li

37

Fleet of Vehicles Mereology

In the traﬃc system that we are building up there are no relations to be expressed between vehicles, only between vehicles and the (single and only) monitor. Thus there is no mereology needed for vehicles.

Attributes ³⁸

We shall model attributes of links, hubs and vehicles. The composite parts, aggregations of hubs, HS and Hs, aggregations of links, LS and Ls and aggregations of vehicles,VS and Vs, also have attributes, but we shall omit modelling them here.

39

Attributes of Links

10. The following are attributes of links.

(a) Link states,lσ:LΣ, which we model as possibly empty sets of pairs of distinct identiﬁers of the connected hubs. A link state expresses the directions that are open to traﬃc across a link.

(b) Link state spaces, lω:LΩ which we model as the set of link states. A link state space expresses the states that a link may attain across time.

(c) Further link attributes are length, location, etcetera.

Link states are usually dynamic attributes whereas link state spaces, link length and link location (usually some curvature rendition) are considered static attributes.

40

type

10a. LΣ= (HI×HI)-set axiom

10a. ∀lσ:LΣ^• 0≤cardlσ≤2 value

10a. attrLΣ: L→LΣ axiom

10a. ∀l:L^• let{hi,hi^′}=mereo L(l)in attrLΣ(l)⊆{(hi,hi^′),(hi^′,hi)} end type

10b. LΩ= LΣ-set value

10b. attr LΩ: L→LΩ axiom

10b. ∀ l:L^• let{hi,hi^′}=mereo L(l)inattr LΣ(l)∈attr LΩ(l)end type

10c. LOC, LEN,...

(27)

value

10c. attrLOC: L→LOC, attrLEN: L →LEN, ...

41

Attributes of Hubs

11. The following are attributes of hubs:

(a) Hub states, hσ:HΣ, which we model as possibly empty sets of pairs of identiﬁers of the connected links. A hub state expresses the directions that are open to traﬃc across a hub.

(b) Hub state spaces, hω:HΩ which we model as the set of hub states. A hub state space expresses the states that a hub may attain across time.

(c) Further hub attributes are location, etcetera.

Hub states are usually dynamic attributes whereas hub state spaces and hub location are considered

static attributes. 42

type

11a. HΣ= (LI×LI)-set value

11a. attrHΣ: H→HΣ axiom

11a. ∀h:H^• attrHΣ(h)⊆{(li,li^′)|li,li^′:LI^•{li,li^′}⊆mereoH(h)}

type

11b. HΩ= HΣ-set value

11b. attr HΩ: H →HΩ axiom

11b. ∀ h:H^• attrHΣ(h)∈attrHΩ(h) type

11c. LOC,...

value

11c. attrLOC: L→LOC, ...

43

Attributes of Vehicles

12. Dynamic attributes of vehicles include (a) position

i. at a hub (about to enter the hub — referred to by the link it is comingfrom, thehub it is at and thelink it is going to, all referred to by their uniqueidentiﬁers or

ii. some fraction “down” a link (moving in the direction from afromhub to atohub — referred to by their uniqueidentiﬁers)

iii. where we model fraction as a real between 0 and 1 included.

(b) velocity, acceleration, etcetera.

13. All these vehicle attributes can be observed.

44

type

12a. VP = atH|onL

12(a)i. atH :: ﬂi:LI×hi:HI×tli:LI

12(a)ii. onL :: fhi:HI ×li:LI×frac:FRAC×thi:HI

12(a)iii. FRAC =Real, axiom∀frac:FRAC^• 0≤frac≤1 12b. VEL, ACC, ...

value

13. attrVP:V→VP, 13. attronL:V→onL,

(28)

13. attratH:V→atH 13. attrVEL:V→VEL, 13. attrACC:V→ACC 13. ...

45

Vehicle Positions

14. Given a net,n:N, we can deﬁne the possibly inﬁnite set of potential vehicle positions on that net,vps(n).

(a) vps(n)is expressed in terms of the links and hubs of the net.

(b) vps(n)is the (c) union of two sets:

i. the potentially³inﬁnite set of “on link” positions ii. for all links of the net

and

iii. the ﬁnite set of “at hub” positions iv. for all hubs in the net.

46

value

14. vps: N→VP-infset 14b. vps(n)≡

14a. let ls=obs Ls(obs LS(n)), hs=obsHs(obs HS(n))in 14(c)i. { onL(fhi,uid(l),f,thi)| fhi,thi:HI,l:L,f:FRAC^• 14(c)ii. l ∈ls∧ {fhi,thi}=mereo L(l) }

14c. ∪

14(c)iii. {atH(fli,uid H(h),tli)|fli,tli:LI,h:H^• 14(c)iv. h∈hs∧ {fli,tli}⊆mereo H(h)}

14a. end

47

Vehicle Assignments

Given a net and a ﬁnite set of vehicles we can distribute these vehicles over the net, i.e., assign initial vehicle positions, so that no two vehicles “occupy” the same position, i.e., are “crashed” ! Let us call the non-deterministic assignment functionvpr.

15. vpm:VPM is a bijective map from vehicle identiﬁers to (distinct) vehicle positions.

16. vpr has the obvious signature.

(a) vpr(vs)(n)is deﬁned in terms of

(b) a non-deterministic selection,vpa, of vehicle positions, and

(c) a non-deterministic assignment of these vehicle positions to vehicle identiﬁers, (d) being the resulting distribution.

48

type

15. VPM^′ = VI →m VP

15. VPM ={|vpm:VPM^′ ^•card domvpm =card rngvpm|}

value

16. vpr: V-set ×N→VMP 16a. vpr(vs)(n)≡

16b. let vpa:VP-set^•vpa⊆vps(vs)(n)∧cardvpa = vard vsin 16c. letvpm:VPM^•dom vpm = vps∧rngvpm = vpain 16d. vpmend end

3 The ‘potentiality’ arises from the nature of FRAC. If fractions are chosen as, for example, 1/5’th, 2/5’th, ..., 4/5’th, then there are only a finite number of “on link” vehicle positions. If instead fraction are arbitrary infinitesimal quantities, then there are infinitely many such.

(29)

Definitions of Auxiliary Functions ⁴⁹ 17. From a net we can extract all its link identiﬁers.

18. From a net we can extract all its hub identiﬁers.

value

17. xtr LIs: N→LI-set

17. xtr LIs(n)≡ {uidL(l)|l:L^•l∈obsLs(obsLS(n))}

18. xtr HIs: N→HI-set

18. xtr HIs(n)≡ {uid H(l)|h:H^•h ∈obsHs(obs HS(n))}

19. Given a link identiﬁer and a net get the link with that identiﬁer in the net.

20. Given a hub identiﬁer and a net get the hub with that identiﬁer in the net.

50

value

22. get H: HI→N→^∼ H

22. get H(hi)(n) ≡ιh:H^•h∈obs Hs(obs HS(n))∧uid H(h)=hi 22. pre: hi∈xtr HIs(n)

22a. get L: LI→N→^∼ L

22a. get L(li)(n)≡ιl:L^•l ∈obsLs(obs LS(n))∧uid L(l)=li 22a. pre: hl∈xtr LIs(n)

Theιa:A^•P(a)expression yields the unique valuea:Awhich satisﬁes the predicate P(a). If none, or more than one exists then the function is undeﬁned.

Some Derived Traffic System Concepts 51

Maps

21. A road map is an abstraction of a road net. We deﬁne one model of maps below.

(a) A road map, RM, is a finite definition set function, that is, a specification language map from

• hub identiﬁers (the source hub)

• to finite definition set maps from link identifiers

• to hub identiﬁers (the target hub).

type

21a. RM^′ = HI →m (LI →m HI)

If a hub identiﬁer in the deﬁnition set or anrm:RMmaps into the empty map then the designated

hub is “isolated”: has no links emanating from it. ⁵²

22. These road maps are subject to a well-formedness criterion.

(a) The target hubs must be deﬁned also as source hubs.

(b) If a link is defined from source hub (referred to by its identifier) shivia linklito a target hubthi, then, vice versa, linkliis also defined from sourcethito targetshi.

type

22. RM ={|rm:RM^′^• wf RM(rm)|}

value

22. wf RM: RM^′ →Bool 22. wf RM(rm)≡

22a. ∪ { rng(rm(hi))|hi:HI^•hi∈dom rm} ⊆domrm 22b. ∧ ∀ shi:HI^•shi∈dom rm⇒

22b. ∀ li:LI^•li ∈dom rm(shi)⇒

22b. li∈dom rm((rm(shi))(li))∧(rm((rm(shi))(li)))(li)=shi

(30)

53

23. Given a road net,n, one can derive “its” road map.

(a) Let hsandlsbe the hubs and links, respectively of the netn.

(b) Every hub with no links emanating from it is mapped into the empty map.

(c) For every link identiﬁeruid L(l)of links,l, oflsand every hub identiﬁer,hi, in the mereology of l

(d) hiis mapped into a map fromuid L(l)intohi’

(e) wherehi’is the other hub identiﬁer of the mereology of l.

54

value

23. derive RM: N→RM 23. derive RM(n)≡

23a. leths =obsHs(obs HS(n)), ls =obs Ls(obs LS(n))in 23b. [ hi7→[ ]|hi:HI^• ∃h:H^•h∈hs∧mereo H(h) ={} ] ∪ 23d. [ hi7→[ uidL(l)7→hi^′

23e. |hi^′:HI^•hi^′=mereo L(l)\{hi} ] 23c. |l:L,hi:HI^•l∈ls∧hi ∈mereo L(l) ]end

Theorem:If the road net,n, is well-formed thenwf RM(derive RM(n)).

Traffic Routes ⁵⁵

24. A traﬃc route,tr, is an alternating sequence of hub and link identiﬁers such that

(a) li:LIis in the mereology of the hub,h:H, identiﬁed byhi:HI, the predecessor of li:LIin route r, and

(b) hi’:HI, which followsli:LIin router, is diﬀerent fromhi, and is in the mereology of the link identiﬁed byli.

type

24. R^′= (HI|LI)^∗

24. R ={|r:R^′ ^•∃n:N^•wf R(r)(n) |}

value

24. wf R: R^′→N→Bool 24. wf R(r)(n)≡

24. ∀i:Nat^•{i,i+1}⊆indsr⇒

24a. is HI(r(i))⇒is LI(r(i+1))∧r(i+1)∈mereo H(get H(r(i))(n)), 24b. is LI(r(i))⇒is HI(r(i+1))∧ r(i+1)∈mereo L(get L(r(i))(n))

56

25. From a well-formed road map (i.e., a road net) we can generate the possibly inﬁnite set of all routes through the net.

(a) Basis Clauses:

i. The empty sequence of identiﬁers is a route.

ii. The one element sequences of link and hub identiﬁers of links and hubs of a road map (i.e., a road net) are routes.

iii. If hi maps into someli inrmthenhhi,liiandhli,hiiare routes of the road map (i.e., of the road net).

(b) Induction Clause:

i. Let rbhiiandhi^′ibr^′ be two routes of the road map.

ii. If the identiﬁers iandi^′ are identical, thenrbhiibr^′ is a route.

(c) Extremal Clause:

i. Only such routes that can be formed from a ﬁnite number of applications of the above clauses are routes.

57

(31)

value

25. gen routes: RM→Routes-infset 25. gen routes(rm)≡

25(a)i. let rs ={hi}

25(a)ii. ∪ {hli,hii,hhi,lii|li:LI,hi:HI^•hi∈dom rm∧rm(hi)=li}

25(b)i. ∪ {letrbhlii,hli^′ibr^′:R^• {rbhlii,hli^′ibr^′}⊆rs∧li=li^′,

25(b)i. r^′′bhhii,hhi^′ibr^′′′:R^•{r^′′bhhii,hhi^′ibr^′′′}⊆rs∧hi=hi^′ in 25(b)ii. rbhliibr^′,r^′′bhhiibr^′′′ end}in

25(c)i. rsend

58

Circular Routes

26. A route is circular if the same identiﬁer occurs more than once.

value

26. is circular route: R→Bool

26. is circular route(r)≡ ∃i,j:Nat ^•{i,j}⊆indsr∧i6=j⇒r(i)=r(j)

59

Connected Road Nets

27. A road net is connected if there is a route from any hub (or any link) to any other hub or link in the net.

27. is conn N: N→Bool 27. is conn N(n)≡

27. letrm = derive RM(n)in 27. letrs = gen routes(rm)in

27. ∀i,i^′:(LI|HI)^•i6=i^′∧{i,i^′}⊆xtr LIs(n)∪xtr HIs(n) 27. ∃r:R^• r∈rs∧r(1)=i∧r(len r)=i^′end end

60

Set of Connected Nets of a Net

28. The set,cns, of connected nets of a net,n, is (a) the smallest set of connected nets,cns,

(b) whose hubs and links together “span” those of the netn.

value

28. conn Ns: N→N-set 28. conn Ns(n)ascns 28a. pre: true

28b. post: conn spans HsLs(n)(cns)

28a. ∧ ∼∃kns:N-set^•card kns<card cns 28a. ∧conn spans HsLs(n)(kns)

61

28b. conn spans HsLs: N→N→Bool 28b. conn spans HsLs(n)(cns)≡

28b. ∀ cn:N^•cn∈cns⇒is connected N(n)(cn)

28b. ∧let (hs,ls) = (obs Hs(obs HS(n)),obs Ls(obs LS(n))), 28b. chs =∪{obsHs(obs HS(cn))|cn∈cns},

28b. cls =∪{obs Ls(obs LS(cn))|cn∈cns} in 28b. hs = chs ∧ls = cls end

62

(32)

Route Length

29. The length attributes of links can be (a) added and subtracted,

(b) multiplied by reals to obtain lengths, (c) divided to obtain fractions,

(d) compared as to whether one is shorter than another, etc., and (e) there is a “zero length” designator.

value

29a. +,−: LEN×LEN→LEN 29b. ∗ : LEN×Real→LEN 29c. / : LEN×LEN→Real

29d. <,≤,=,6=,≥,>: LEN×LEN→Bool 29e. ℓ0 : LEN

63

30. One can calculate the length of a route.

value

30. length: R→N→LEN 30. length(r)(n)≡

30. caserof: 30. hi →ℓ0, 30. hsiibr^′ →

30. is LI(si)→attrLEN(get L(si)(n))+length(r^′)(n) 30. is HI(si)→length(r^′)(n)

30. end

64

Shortest Routes

31. There is a predicate,is R, which,

(a) given a net and two distinct hub identiﬁers of the net, (b) tests whether there is a route between these.

value

31. is R: N→(HI×HI)→Bool 31. is R(n)(fhi,thi)≡

31a. fhi6= thi∧ {fht,thi}⊆xtr HIs(n)

31b. ∧ ∃r:R ^•r∈routes(n)∧hdr = fhi∧r(lenr) = thi

65

32. The shortest between two given hub identiﬁers (a) is an acyclic route,r,

(b) whose ﬁrst and last elements are the two given hub identiﬁers (c) and such that there is no route,r^′ which is shorter.

value

32. shortest route: N→(HI×HI) →R 32a. shortest route(n)(fhi,thi)asr 32b. pre: pre shortest route(n)(fhi,thi) 32c. post: pos shortest route(n)(r)(fhi,thi)

66

(33)

32b. pre shortest route: N→(HI×HI)→Bool 32b. pre shortest route(n)(fhi,thi)≡

32b. is R(n)(fhi,thi) ∧fhi6=thi∧ {fhi,thi}⊂xtr HIs(n) 32c. pos shortest route: N→R →(HI×HI)→Bool 32c. pos shortest route(n)(r)(fhi,thi)≡

32c. r∈routes(n)

32c. ∧ ∼∃r^′:R^•r^′ ∈routes(n)∧length(r^′)<length(r)

States ⁶⁷

There are diﬀerent notions of state. In our example these are some of the states: the road net composition of hubs and links; the state of a link, or a hub; and the vehicle position.

1.2.2 Perdurants ⁶⁸

For pragmatic reasons we analyse three kinds of perdurants: actions, events and behaviours.

Actions 69

An action is what happens when a function invocation changes, or potentially changes a state.

Examples of traﬃc system actions are:insertion ofhubs,insertion oflinks,removal ofhubs,removal of links, setting of hub state (hσ), moving a vehicle along a link, stopping a vehicle, starting a vehicle,moving a vehicle from a link to a hub andmoving a vehicle from a hub to a link. Here we shalljust illustrate one of these actions. Later, in Sect. 1.2.2, we shall illustrate the vehicle actions.

70

33. Theinsertaction applies to a net and a hub and conditionally yields an updated net.

(a) The condition is that there must not be a hub in the “argument” net with the same unique hub identiﬁer as that of the hub to be inserted and

(b) the hub to be inserted does not initially designate links with which it is to be connected.

(c) The updated net contains all the hubs of the initial net “plus” the new hub.

(d) and the same links.

71

value

33. ins H: N→H→^∼ N

33. ins H(n)(h)asn^′,pre: pre ins H(n)(h),post: post ins H(n)(h) 33a. pre ins H(n)(h) ≡

33a. ∼∃h^′:H^• h^′ ∈obs Hs(n)∧uidHI(h)=uid HI(h^′) 33b. ∧mereo H(h) ={}

33c. post ins H(n)(h)(n^′)≡

33c. obsHs(n) ∪ {h} =obs Hs(n^′) 33d. ∧obs Ls(n) =obs Ls(n^′)

We leave it as exercises to deﬁne the other hub and link actions.

(34)

Events ⁷²

By anevent we understand a state change resulting indirectly from an unexpected application of a function, that is, that function was performed “surreptitiously”. Events can be characterised by a pair of (before and after) states, a predicate over these and, optionally, a timeortime interval.

Events are thus like actions: change states, but are usually either caused by “previous” actions, or

caused by “an outside action”. ⁷³

34. Link disappearance is expressed as a predicate on the “before” and “after” states of the net.

The predicate identiﬁes the “missing” ℓink (!).

34. link dis: N×N→Bool 34. link dis(n,n^′)≡

34. ∃ℓ:L^•pre link dis(n,ℓ)⇒post link dis(n,ℓ,n^′) 35. pre link dis: N×L →Bool

35. pre link dis(n,ℓ)≡ℓ ∈obs Ls(n)

74

35. Before the disappearance of linkℓin net n (a) the hubsh^′ andh^′′ connected to link ℓ

(b) were connected to links identiﬁed by {l^′₁, l₂^′, . . . , l^′p}respectively{l^′′₁, l^′′₂, . . . , l^′′q} (c) where, for example,l_i^′, l_j^′′are the same and equal touid Π(ℓ).

75 36. After linkℓdisappearance there are instead (a) two separate links, ℓi andℓj, “truncations” ofℓ (b) and two new hubsh^′′′ andh^′′′′

(c) such thatℓi connectsh^′ and h^′′′ and (d) ℓj connectsh^′′andh^′′′′.

37. Existing hubsh^′ andh^′′ now have mereology

(a) {l^′₁, l^′₂, . . . , l^′_p} \ {uid Π(ℓ)} ∪ {uidΠ(ℓi)}respectively (b) {l^′′₁, l^′′₂, . . . , l_q^′′} \ {uidΠ(ℓ)} ∪ {uid Π(ℓj)}

38. All other hubs and links ofnare unaﬀected.

We shall not express the above properties explicitly. Instead we expect such a predicate to hold for the interpretation now give.

76

39. We shall “explain”link disappearanceas the combined, instantaneous eﬀect of (a) ﬁrst aremove link“event” where theremoved linkconnectedhubshij andhik; (b) then the insertion of two new, “fresh”hubs,hαandhβ;

(c) “followed” by theinsertion of two new, “fresh” linksljα andlkβ such that i. ljα connectshij andhαand

ii. lkβ connectshik andhkβ.

77

value

39. post link dis(n,ℓ,n^′)≡ 39. let(h a,h b):H×H^•

39. let{li a,li b}=mereo L(ℓ)in

39. (get H(li a)(n),get H(li b)(n))end in 39a. let n^′′ = rem L(n)(uid L(ℓ))in 39b. let hα,hβ:H ^• {hα,hβ} ∩obs Hs(n)={}in 39b. let n^′′′ = ins H(n^′′)(hα)in

39b. let n^′′′′ = ins H(n^′′′)(hβ)in

39c. letljα,lkβ:L ^• {ljα,lkβ} ∩obs Ls(n)={}

39c. ∧mereo L(ljα) ={uidH(h a),uid H(hα)}

39c. ∧mereo L(lkβ) = {uid H(h b),uidH(hβ)} in 39(c)i. let n^{′′′′′} = ins L(n^′′′′)(ljα)in

39(c)ii. n^′ = ins L(n^{′′′′′})(lkβ)end end end end end end end

(35)

Behaviours ⁷⁸ Traffic

Continuous Traffic

For the road traffic system perhaps the most significant example of a behaviour is that of its traffic:

40. the continuous time varying discrete positions of vehicles,vp:VP⁴, 41. where time is taken as a dense set of points.

type 41. cT

40. cRTF = cT→(V →m VP)

79

Discrete Traffic

We shall model, not continuous time varying traﬃc, but 42. discrete time varying discrete positions of vehicles,

43. where time can be considered a set of linearly ordered points.

43. dT

42. dRTF = dT →m (V →m VP)

44. The road traﬃc that we shall model is, however, of vehicles referred to by their unique iden- tiﬁers.

type

44. RTF = dT →m (VI →m VP)

80

Time: An Aside

We shall take a rather simplistic view of time [27, 75, 86, 102].

45. We considerdT, or justT, to stand for an ordered set of time points.

46. And we considerTIto stand for time intervals based onT.

47. We postulate an inﬁnitesimal small time intervalδ.

48. T, in our presentation, has lower and upper bounds.

49. We can compare times and we can compare time intervals.

50. And there are a number of “arithmetics-like” operations on times and time intervals.

81

type 45. T 46. TI value 47. δ:TI

48. MIN,MAX:T→T

48. <,≤,=,≥,>: (T×T)|(TI×TI)→Bool 49. −:T×T→TI

50. +:T×TI,TI×T→T 50. −,+:TI×TI→TI 50. ∗:TI×Real→TI 50. /:TI×TI→Real

82 4 ForVPsee Item 12a on Page 9.

(36)

Global Clock

51. We postulate a globalclockbehaviour which oﬀers the current time.

52. We declare a channelclk ch.

value

51. clock:T→outclk ch Unit

51. clock(t)≡...; clk ch!t ;... ; clock(t⌈⌉t+δ) channnel

52. clk ch:T

Globally Observable Parts ⁸³

There is given 53. a net,n:N,

54. a set of vehicles,vs:V-set, and 55. a monitor,m:M.

Then:N,vs:V-setand m:Mare observable from the road traﬃc system domain.

value

53. n:N =obs N(∆)

53. ls:L-set=obs Ls(obs LS(n)), hs:H-set=obs Hs(obs HS(n)), 53. lis:LI-set={uid L(l)|l:L^•l∈ls}, his:HI-set={uid H(h)|h:H^•h∈hs}

54. vs:V-set=obs Vs(obs VS(obs F(∆))), vis:V-set={uidV(v)|v:V^•v∈vs}

55. m:obsM(∆)

Road Traffic System Behaviours ⁸⁴

56. Thus we shall consider our road traﬃc system,rts, as (a) the concurrent behaviour of a number of vehicles, (b) amonitor behaviour,

(c) an initial vehicle position map, and (d) an initial starting time.

85

value

56c. vpm:VPM = vpr(vs)(n) 56d. t0:T = clk ch?

56. rts() =

56a. k {veh(uidV(v))(v)(vpm(uid V(v)))|v:V^•v∈vs}

56b. k mon(m)([ t0 7→vpm ])

where the “extra”monitor argument,rtf:RTF, records the discrete road traﬃc initially set to the singleton map from an initial start time,t0 to the initial assignment of vehicle positions.

Channels ⁸⁶

In order for the monitor behaviour to assess the vehicle positions these vehicles communicate their positions to the monitor via a vehicle to monitor channel. In order for the monitor to time-stamp these positions it must be able to “read” a clock.

57. Thus we declare a set of channels indexed by the unique identiﬁers of vehicles and communicating vehicle positions.

channel

57. {vm ch[ vi ]|vi:VI^•vi∈vis}:VP

(37)

Behaviour Signatures ⁸⁷

58. The road traﬃcsystem behaviour, rts, takes no arguments (hence the ﬁrst Unit); and “behaves”, that is, continues, forever (hence the last Unit).

59. Thevehicle behaviours are indexed by the unique identiﬁer,uid V(v):VI, thevehicle part,v:V and the vehicle position; oﬀers communication to themonitor behaviour (on channelvm ch[vi]);

and behaves “forever”.

60. The monitor behaviour takes the so far unexplained monitor part, m:M, as one argument and the discrete road traﬃc, drtf:dRTF, being repeatedly “updated” as the result of input communications from (all) vehicles; the behaviour otherwise runs forever.

value

58. rts:Unit→Unit

59. veh: vi:VI→v:V →VP →outvm ch[ vi ],mi:MI Unit

60. mon: m:M→RTF→in{vm ch[ vi ]|vi:VI^•vi∈vis},clk ch Unit

The Vehicle Behaviour ⁸⁸

61. Avehicle process is indexed by the unique vehicle identiﬁervi:VI, the vehicle “as such”,v:V and the vehicle position,vp:VPos.

The vehicle process communicates with the monitor process on channel vm[vi] (sends, but receives no messages), and otherwise evolves “in[de]ﬁnitely” (hence Unit). 89

62. We describe here an abstraction of the vehicle behaviourataHub (hi).

(a) Either the vehicle remains at that hub informing the monitor, (b) or, internally non-deterministically,

i. moves onto a link, tli, whose “next” hub, identiﬁed by thi, is obtained from the mereology of the link identiﬁed bytli;

ii. informs the monitor, on channelvm[vi], that it is now on the link identiﬁed bytli, iii. whereupon the vehicle resumes the vehicle behaviour positioned at the very beginning

(0) of that link,

(c) or, again internally non-deterministically, (d) the vehicle “disappears — oﬀ the radar” !

90

62. veh(vi)(v)(vp:atH(ﬂi,hi,tli))≡ 62a. vm ch[ vi ]!vp ; veh(vi)(v)(vp)

62b. ⌈⌉

62(b)i. let{hi^′,thi}=mereo L(get L(tli)(n))in assert:hi^′=hi 62(b)ii. vm ch[ vi ]!onL(tli,hi,0,thi) ;

62(b)iii. veh(vi)(v)(onL(tli,hi,0,thi))end

62c. ⌈⌉

62d. stop

91

63. We describe here an abstraction of the vehicle behaviouron aLink (ii).

Either

(a) the vehicle remains at that link position informing the monitor, (b) or, internally non-deterministically,

(c) if the vehicle’s position on the link has not yet reached the hub,

i. then the vehicle moves an arbitrary increment δalong the link informing the monitor of this, or

ii. else, while obtaining a “next link” from the mereology of the hub (where that next link could very well be the same as the link the vehicle is about to leave),

A. the vehicle informs the monitor that it is now at the hub identiﬁed bythi, B. whereupon the vehicle resumes the vehicle behaviour positioned at that hub.

(38)

64. or, internally non-deterministically, 65. the vehicle “disappears — oﬀ the radar” !

92

61. veh(vi)(v)(vp:onL(fhi,li,f,thi))≡ 63a. vm ch[ vi ]!vp ; veh(vi)(v)(vp) 63b. ⌈⌉

63c. iff +δ<1

63(c)i. thenvm ch[ vi ]!onL(fhi,li,f+δ,thi) ; 63(c)i. veh(vi)(v)(onL(fhi,li,f+δ,thi))

63(c)ii. else letli^′:LI^•li^′ ∈mereo H(get H(thi)(n))in 63(c)iiA. vm ch[ vi ]!atH(li,thi,li^′);

63(c)iiB. veh(vi)(v)(atH(li,thi,li^′))end end

64. ⌈⌉

65. stop

The Monitor Behaviour ⁹³

66. Themonitor behaviour evolves around the attributes of an own “state”,m:M, a table of traces of vehicle positions, while accepting messages about vehicle positions and otherwise progressing

“in[de]ﬁnitely”.

67. Either the monitor “does own work”

68. or, internally non-deterministically accepts messages from vehicles.

(a) A vehicle position message,vp, may arrive from the vehicle identiﬁed byvi.

(b) That message is appended to that vehicle’s movement trace, (c) whereupon the monitor resumes its behaviour —

(d) where the communicating vehicles range over all identiﬁed vehicles.

94

66. mon(m)(rtf)≡

67. mon(own mon work(m))(rtf) 68. ⌈⌉

68a. ⌈⌉⌊⌋ {let((vi,vp),t) = (vm ch[ vi ]?,clk ch?)in

68b. letrtf^′ = rtf†[ t 7→rtf(maxdom rtf)†[ vi7→vp ] ]in 68c. mon(m)(rtf^′)end

68d. end|vi:VI^• vi∈vis} 67. own mon work: M→RTF→M

1.3 Whither Domain Science & Engineering ?

⁹⁵

In a 2006 e-mail, in response, undoubtedly to my steadfast, perhaps conceived as stubborn in- sistence, on domain engineering, Tony Hoare summed up his reaction to domain engineering as follows, and I quote⁵:

“There are many unique contributions that can be made by domain modelling.

1. The models describe all aspects of the real world that are relevant for any good software design in the area. They describe possible places to define the system boundary for any particular project.

2. They make explicit the preconditions about the real world that have to be made in any embedded software design, especially one that is going to be formally proved.

96

5 E-Mail to Dines Bjørner, CC to the late Robin Milner et al., July 19, 2006