Beweren en bewijzen/de zuilen/Formalisering/6. Tijd

literatuur ...

Real-timesystemen zijn systemen die precies op tijd moeten reageren. Ze zijn vaak ingebouwd in machines, liften, verkeersregelingsinstallaties e.d. In Nijmegen doet de Informatica voor Technische Toepassingen hieromtrent veel onderzoek. Eigenlijk zijn, als je het goed bekijkt, alle systemen real-timesystemen, ook een salarisadministratie: als je salaris immers niet elke maand komt, is het fout. Maar niet bij elk systeem vindt men timing zo belangrijk en critisch dat men er in de correctheidsstelling aandacht aan besteedt. De Postbank zette bijvoorbeeld jaren lang elke avond om 23:00 het programma aan dat alle overschrijvingen van die dag verwerkt, en dat was gewoon een paar uur later klaar omdat tegenwoordig computers snel genoeg zijn. Men denkt na over correctheid van het beheer van alle rekeningen, er mag bij het overschrijven geen geld ontstaan of verloren gaan, er mag niets twee keer overgeschreven worden, maar "tijd speelt geen rol" omdat de nacht tussen twee werkdagen altijd lang genoeg was.

Bij systemen als een spoorwegovergang met lichten en slagbomen speelt tijd een cruciale rol. We pakken dat systematisch aan.

Keuze van een tijdsmodel

Als we gedrag willen specificeren waarbij tijd een rol speelt, moeten we als onderdeel van ons domeinmodel een geschikte wiskundige structuur voor de tijd kiezen. Hier een paar voorbeelden:

• De belastingdienst werkt met kalenderjaren. Voor specificaties van delen van het belastingstelsel zijn jaargetallen als tijdsmodel voldoende.
• Rente van spaarrekeningen wordt per dag berekend. Een tijdsmodel waarbij men over uren en minuten moet praten kan de zaak nodeloos ingewikkeld maken.
• Een ouderwetse wijzerklok zonder datumtelling doet elk etmaal tweemaal precies hetzelfde. Een klok met een slinger van 1 m heeft seconden als kleinste eenheid. Om te beredeneren of een bepaald raderwerk een correcte klok oplevert, zijn hele getallen modulo 12*60*60 het meest geschikt: de seconden van een halve dag.
• Binnen een vak als computerarchitectuur kan het adequaat zijn, alles te specificeren in termen van de klok van de processor.
• Natuurkundigen modelleren tijd als reële getallen, met als eenheid de seconde. Als het in je werkstuk niet gaat om kalenderdagen en processorklokcycli maar om snelheden van voertuigen en duraties van processen als het openen van deuren, is dit misschien het meest voor de hand liggende tijdsmodel.

Je maakt een keuze en neemt in je domeinmodel een type T op met de nodige uitleg, bijvoorbeeld: "Natuurlijke getallen, eenheid sec".

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in sec. in reële getallen		Definition T := R.

Observaties

De predikaten van het domeinmodel komen overeen met observeerbare gebeurtenissen in de reële wereld. Het predikaat is_mannelijk x is bijvoorbeeld waar als persoon x in de werkelijkheid inderdaad mannelijk is. We maken een observatie (natuurkundig: een meting) en weten of het predikaat waar of onwaar is.

Als tijd een rol speelt, verdient het aanbeveling, de predikaten van het domeinmodel te voorzien van een tijdparameter:

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in sec. in reële getallen		Definition T := R.
S		de toestanden van sensoren: {actief, passief}		Variable S:Set. Variable actief:S. Variable passief:S.
D		de toestanden van slagbomen: {open, bewegend, dicht}		Variable D:Set. Variable open:D. Variable bewegend:D. Variable dicht:D.
predicaat	type	betekenis	meting	formele notatie
treinsensor	T→S→B	treinsensor t actief: op moment t zendt de treinsensor een puls treinsensor t passief: op moment t zendt de treinsensor geen puls	5 Volt op de sensorkabels 0 Volt op de sensorkabels	Variable treinsensor:T->S->B.
boom	T→D→B	boom t open: op moment t staan de bomen recht omhoog (5 graden omprecies te zijn) boom t bewegend: op moment t bewegen de bomen boom t dicht : op moment t staan de bomen horizontaal	kijken	Variable boom:T->D->B.

Loop je lijst van gegeven predikaten af en kijk welke op één moment waar, op een ander moment onwaar kunnen zijn; zij komen in aanmerking voor een tijdparemeter. Overigens: gezien dat steeds meer mensen tijdens hun leven van geslacht veranderen is het een kwestie van tijd dat de burgerlijke stand ook overgaat tot predicaten met een tijdsparameter: is_mannelijk datum x

Eigenlijk kom je bij het specificeren van real-timesystemen uit met één predikaat met drie parameters: wanneer, waar, wat. Je moet dan wel voor elke mogelijke waarde aangeven hoe deze gemeten kan worden.

type		betekenis (verzameling)
T		de tijd: Natuurlijke getallen, eenheid sec
L		de observatiepunten: zie lijst van observatiepunten
V		alle mogelijke waarden en toestanden: zie tabel van metingen
predicaat	type	betekenis	meting
obs	T→L→V→B	obs t l v: op observatiepunt l is op moment t de waarde v observeerbaar	zie tabel van metingen

Of je alles in termen van zo'n algemene obs specificeert of diverse predikaten als treinsensor als gegeven aanneemt, is grotendeels een kwestie van smaak. Je kunt ook het ene in je domeinmodel opnemen en het andere definiëren:

Definition treinsensor (t:T) (s:V) := obs t sensor s.

Echte tijd en representaties

Leer te onderscheiden tussen de fysieke tijd, d.w.z. de momenten waarop in de realiteit iets gebeurt en geobserveerd kan worden, en de representatie van momenten en duraties in het geheugen van een systeem.

Een kookwekker rinkelt op bepaalde momenten. Dat is de fysieke tijd. Op dat moment kun je iets observeren. Je kunt "een tijd instellen", maar dat is niet de fysieke tijd, dat is een wijzerpositie, of een cijfer op een schermpje. Op een bepaald moment kun je observeren dat het wijzertje op een bepaalde stand staat. Het is een instelling die een poos dezelfde blijft en die de gewenste kooktijd representeert. Als je een kookwekker op moment t instelt op kooktijd d, schrijf je zet t (repr d) om het verschil duidelijk te maken. t is onze tijdsparameter en geeft het daadwerkelijke moment aan waarop de handeling van het instellen plaats vindt. repr d is de representatie van een kooktijd, bijvoorbeeld in de vorm van de positie van een instelschroef. De functie repr moet je uiteraard wel definiëren.