Reaaliaika.

Oletetaan, että järjestelmä koostuu komponenteista. Komponentti on automaatti, jolla on oma tilojen joukko, ja se siirtyy tilasta toiseen suorittamalla tapahtumia. Otetaan yksinkertainen malli, jossa jokaiseen tapahtumaan liitetään kello. Kello on muuttuja, joka saa ei-negatiivisia reaalilukuarvoja. Kun tapahtuma tapahtuu, niin siihen liitetty kello nollataan. Tapahtumalla on lisäksi esiehto,  joka kertoo, milloin tapahtuma voi tapahtua. Tämä esiehto on konjunktio erilaisista yksinkertaisista kelloja koskevista epäyhtälöistä, kuten vaikka että "x < 5 ja y > 3". Tällaiset ehdot tulkitaan niin, että jotta tämä tapahtuma voi tapahtua, kellon x näyttämän arvon  pitää olla pienempi kuin 5 ja kellon y näyttämän arvon suurempi kuin 3.

Erilaisia kelloyhdistelmiä ja aikoja on äärettömän paljon, jopa ylinumeroituvasti, koska kellot ovat reaaliarvoisia. Jos kuitenkin oletamme, että esiehdoissa esiintyy vain kokonaislukuja, relevanttien yhdistelmien määrä putoaa numeroituvaksi. Itse arvoja tietenkin on edelleen ylinumeroituvasti, mutta tapahtumien esiehtojen päälle- ja poiskytkeytymisiä on numeroituva määrä. Ja itseasiassa, niitä on äärellinen määrä jokaisessa tilassa, mikä on myös helppo nähdä. Jos esitämme mahdolliset kellojen arvot ns alueina, niin voimme esittää sekä kellojen että tilojen konfiguraatiot äärellisesti.

Jos kelloja on n kappaletta, niin alue on n-ulotteinen monitahokas, jonka määrittelevät kelloehdot jotka ovat muotoa x - y < k (tai x - y ≤ k) , missä x ja y ovat mielivaltaisia kelloja, kun mukana on myös "dummykello", joka näyttää aina arvoa 0. Alue voidaan siis esittää (n+1)*(n+1)- matriisina. Tälle matriisille on kanoninen esitysmuoto, josta käytetään nimeä Difference Bound Matrix.

Jos Z on alue, jossa järjestelmä on, ja suoritamme tapahtuman a, niin ensimmäiseksi tiedämme, että a:n esiehdon pitää päteä; se ei välttämättä päde koko Z:ssa. Olkoon Z(a) se osa Z:sta, jossa esiehto pätee. Tämän jälkeen nollataan a:han liittyvä kello, ja saadaan jälleen uusi alue, Z(a0). Tämän jälkeen Z(a0) laajennetaan kattamaan kaikki ne kelloyhdistelmät, jotka saadaan kun ajan annetaan kulua, merkitään tätä aluetta Z*. Z* on nyt se alue, johon päädytään suorittamalla a. Tämän lisäksi tietysti järjestelmän tila muuttuu.

Ongelmaksi tulee se, että tämä abstraktio on kovin tiukka. Se erottelee kovin paljon siitä, mitä systeemi voi tehdä. Jos esimerkiksi tapahtumat a ja b ovat täysin toisistaan riippumattomia, ja olemme jossakin tilassa, vieläpä niin, että kun tapahtumat a ja b tapahtuvat ja päädymme samaan tilaan, tämä abstraktio "muistaa" missä järjestyksessä a ja b tapahtuivat. Yksinkertaisuuden vuoksi viittaan tapahtuman kelloon ja itse tapahtumaan samalla symbolilla, toivon ettei tämä aiheuta sekaannusta.

Oletataan, että aivan alussa a = 0 ja b = 0, ja annamme ajan kulua vapaasti. DBM-esityksessä a:lla ja b:llä ei ole silloin ylärajaa, mutta a-b = 0 ja b-a = 0, koska kellot näyttävät samaa aikaa. Jos a tapahtuu ensin, päädymme alueelle, jossa b-a ei ole rajoitettu ja a - b < 0. Kun b sitten tapahtuu, päädymme aluelle, jossa a-b ei ole rajoitettu mutta b-a < 0. Jos b tapahtuu ensin ja sitten a, päädymme puolestaan alueelle jossa a-b < 0, eikä muuta rajoitusta ole. Tämä tarkoittaa että vaikka järjestelmä muuten olisi suunniteltu niin, että a ja b voivat tapahtua missä järjestyksessä tahansa (esimerkiksi, ne voivat kuvastaa kahta eri napin painamista niin että niiden järjestyksellä ei ole toiminnallista merkitystä, kunhan kumpaakin painetaan ajoissa), joudumme tutkimaan kaksi kertaa niin paljon erilaisia vaihtoehtoja kuin olisi todellisuudessa tarpeen.

Tätä varten tarvitaan abstraktio, joka ideaalitilanteessa yhdistää nämä kaksi aluetta. Vaihtoehtoja tälle on useampia. Yksi on, että kelloja ei nollata ennenkuin kaikki olennaiset tapahtumat ovat tapahtuneet, ja määritellään alua sen jälkeen unionina kaikista niistä alueista, joihin olisi voitu päätyä kun tapahtumat olisi nollattu erikseen. Tämän heikkoutena on, että pitää ikäänkuin etukäteen tietää mitkä kaikki tullaan tutkimaan, eikä voida käyttää perinteisempiä, puhtaasti kontrollirakenteisiin perustuvia vaihdannaisuuden ja riippumattomuuden analysointimenetelmiä.

Toinen on, että yksinkertaisesti unohdamme jotkut kelloista. Emme piittaa rajoitteista jotka viittaavat kelloon a, ja näin kello b ja kello a ovat riippumattomia. Tämän ongelmana on, että se on yliapproksimaationa melko karkea, eli järjestelmän käyttäytymiseen tulee mukaan sellaisia tapahtumaketjuja, jotka eivät todellisuudessa ole mahdollisia, koska kello a toimisi näitä rajoittavana tekijänä.

Kolmas on, että yksinkertaisesti pyyhkäisemme tietyt pareittaiset rajoitteet pois jälkikäteen. Jos a ja b ovat riippumattomia, pyyhimme pois tiedon siitä, mitä a-b ja b-a ovat. Tällöin jäljelle jää rajoitteita muiden kellojen osalta, mutta niistä ei voi päätellä "mitä kello on". Ongelmaksi muodostuu kolmannet kellot: jos a:lla on esiehtona, että c < 5 ja b:llä esiehtona, että c > 5, niin b:n tapahtuminen tekee a:n tapahtumisen mahdottomaksi. a:n on pakko tapahtua ensin. Tätä varten tarvitaan epäsymmetrinen riippuvuusrelaatio: tässä esimerkissä a riippuu b:stä, mutta b ei riipu a:sta. Jos teemme a:n, se ei vaikuta b:hen mitenkään, mutta toisinpäin vaikutus löytyy. Tässäkin abstraktiossa on sellainen puoli, että se tuottaa käyttäytymisiä, jotka eivät ole alkuperäisen systeemin käyttäytymisiä, koska voimme joissain tilanteissa yliabstraktion vuoksi tutkia a:n ja b:n väärässä järjestyksessä.

Korjaamme tämän käyttämällä tekniikkaa joka tunnetaan nimellä abstraktion tarkentaminen (abstraction refinement). Aloitamme aivan liian löyhästä abstraktiosta, joka mahdollistaa jos jonkinlaista käyttäytymistä. Kun sitten löydämme "virheen", pyrimme toistamaan tämän alkuperäisten alueiden avulla. Jos tämä epäonnistuu, niin virheen suorittaminen päätyy alueelle, joka on tyhjä. Tämä on tulkittavissa niin, että tässä ketjussa viimeinen tapahtuma ei ole suoritettavissa, koska sen esiehdot eivät täyty; ne kuitenkin täyttyivät abstrahoidussa versiossa, joten esiehdoissa on oltavat jotakin sellaista, mitä todellinen järjestelmä rajoittaa. Kellojen unohtamisen tapauksessa tiedämme esimerkiksi, että jokin ehto oli unohdettu. Lisäämme jonkin tällaisen rajoitteen abstraktiooon, jolloin siitä tulee tarkempi, ja ajamme tarkastuksen uudelleen.

Koska abstraktio ei koskaan poista käyttäytymistä (mutta voi lisätä sitä), virheettömyyden todistaminen abstraktissa mallissa tarkoittaa ettei alkuperäisessäkään voi olla virheitä. Toisaalta, jos onnistumme suorittamaan abstraktin virheen konkreettisessa mallissa, se on todellinen virhe. On helppo nähdä, että tämä prosessi päättyy lopulta.

Jos oletamme että jokainen abstrahoitu ehto säästää esimerkiksi 20 prosenttia työstä, on tämä prosessi pahimmillaan liki 5 kertaa hitaampi kuin pelkkä tarkastus alunperin konkreettisella järjestelmällä. Jos säästö on 50%, niin pahin tapaus on kaksinkertainen. Mutta me emme välitä pahimmasta tapauksesta, vaan parhaasta tapauksesta. Tällöin voimme voittaa paljonkin jos saamme konkreettisen vastauksen varhaisessa vaiheessa.

Seuraavat viikot olen toteuttamassa järjestelmää joka tekee tämän, ja pyrimme saamaan tulokset valmiiksi niin, että voimme lähettää ne TACASiin.