TheoFoMon: Fræðileg undirstaða fyrir vöktun og sannprófun á keyrslutíma - verkefni lokið

Fréttatilkynning verkefnisstjóra

16.9.2020

En hvernig göngum við úr skugga um að kerfi, sem við höfum þegar búið til, geri það sem þeim er ætlað? Í áratugi hefur þessi lykilspurning verið í fókus í rannsóknum og er enn mikil áskorun og verður sífellt mikilvægari þar sem slík kerfi verða sífellt mikilvægari í lífi okkar. Vöktun á keyrslutíma (e. runtime monitorability) er svið innan tölvunafræði sem gengur út á að tryggja að kerfin, sem við útbúum, geri það sem til er ætlast af þeim. Þessi nálgun byggist á reiknieiningum, sem við köllum vaktara (e. monitors) sem fylgjast með kerfinu sem er til skoðunar, greina þær hendingar sem það framleiðir til þess að ákvarða hvort það hegðar sér eins og til er ætlast og að bregðast við ef svo er ekki. Markmiðið með TheoFoMon verkefninu var að reyna að svara eftirfarandi spurningum og að skoða fræðilegan grunn sviðsins í vöktun á keyrslutíma.

- Hvaða eiginleika hjá kerfum er hægt að vakta á keyrslutíma og með hvers konar vökturum?

- Í kröfulýsingu er ákveðin hegðun sem þarf að vera, hvers konar trygging er fyrir réttri hegðun sem hægt er að vakta?

- Fyrir hvers konar eiginleika kerfa er hægt að þróa vaktara sem geta þvinga fram rétta kerfishegðun á keyrslutíma óháð því hversu villandi hegðun notandans er?

Þær rannsóknir sem gerðar voru í tengslum við þetta verkefni, hafa gefið af sér umgjörð sem nýtist við að svara þeim spurningum sem nefndar eru hér að ofan. Lykilhugmynd fyrir öllum birtingum verkefnisins er að fræðin á bak við vöktun á keyrslutíma byggist á vökturum, sem eru grunneiningarnar sem framkvæma sannprófunina. Þessi nálgun hefur gefið af sér mjög glæsileg fræði um vöktun sem dregur fram eftirfarandi meginniðurstöðu: Þeim mun meiri tryggingu fyrir réttmæti sem við gerum ráð fyrir að vaktararnir gefi okkur, þeim mun færri eiginleikar eru vaktanlegir. 

Auk þess að hafa gefið af sér fimm bækur og útgefin hefti, þrjá bókarkafla, fimm tímaritsgreinar, 20 ráðstefnugreinar, sex annars konar birtingar og sex greinar sem bíða eftir mati, hefur verkefnið gegnt hlutverki sem þjálfunarvettvangur fyrir unga vísindamenn og gefið af sér tvö BSc verkefni, eitt MSc verkefni og tvö PhD verkefni. Tveir ungir vísindamenn, þátttakendur í TheoFoMon hafa fengið fasta akademiska stöðu, á Íslandi og í Frakklandi, og hefur sá styrkleiki sem komið hefur fram í þessu verkefni gegnt lykilhlutverki í því sambandi.

Fræðilegi grunnurinn sem þetta verkefni felur í sér, myndar grunn fyrir "open-sorce" hugúnaðartól fyrir vöktun á keyrslutíma sem útfært er í Erlang og Java og hafa verið notuð í fjölda raunverulegra verkefna. 

Vinnan sem framkvæmd var í þessu verkefni, er líkleg til að hafa áhrif á öryggisviðkvæm kerfi (e. safety-critical systems) í framtíðinni og er ágætur grunnur fyrir framtíðar rannsóknir sem sumar eru nú þegar hafnar í Tölvunarfræðideild Háskólans í Reykjavík og við teljum að eigi bjarta framtíð fyrir sér.

Allar birtingar og hugbúnaðartól, sem eru afurðir þessa verkefnis, eru, og verða, aðgengileg á http://icetcs.ru.is/ þar sem hægt er að nálgast framtíðarupplýsingar um þetta efni.

English version:

Computing systems are everywhere in modern society; they allow us to command, control, communicate, do business, monitor our health, travel and entertain ourselves, among many other things. Such systems are always built for a purpose. Once we build and deploy them, how can we be sure that they behave as expected? This key scientific question has been studied in computer science for decades, but is still a grand challenge whose importance has increased since computing devices are embedded in every aspect of our lives. Runtime monitoring is a field of computer science that deals with the problem of making sure that the actual behavior of the computing devices we deploy is in agreement with the expected one. This approach is based on the use of computational entities, called monitors, that observe the execution of the system under scrutiny and analyse the events it generates in order to determine whether it is misbehaving, and, if so, to take appropriate corrective actions. 

The goal of the TheoFoMon project was to study the theoretical foundations of runtime monitoring by tackling fundamental questions underlying this approach to system validation such as:

• What system properties can be monitored at runtime and by what kind of monitors?

• What are the correctness guarantees that monitors can provide for monitorable specifications?

• For what system properties is it possible to develop monitors that can enforce proper system behavior at runtime regardless of how malicious users of the system can be?

The research carried out within the project has provided a principled framework for answering the aforementioned questions. The key underlying idea that guided all the work presented in the project deliverables is that a theory of monitorability should be based on monitors, which are the entities carrying out the verification. Taking this operational, monitor-based viewpoint has led to the development of an elegant theory of monitorability that highlights the fact that monitorability comes in a spectrum: The more guarantees we expect monitors to give, the fewer the monitorable properties are. 

Apart from producing five books and edited volumes, three book chapters, five journal papers, 20 conference papers, six other types of publications and six papers under submission, the project served as a training ground for your researchers, yielding two BSc theses, one MSc thesis and two PhD theses. Two young researchers contributing to TheoFoMon have obtained permanent positions in Iceland and in France, also based on the scientific strength of the work they carried out in the project.

The theoretical work carried out within the project served as the foundation for the development of open-source software tools for the runtime monitoring of systems written in Erlang and Java, which have been applied in a variety of case studies. The work in this project might have impact on the development of mission- and safety-critical systems and provides an excellent basis for future research, some of which has already started at the Department of Computer Science at Reykjavik University. We confidently expect a bright future for research and applications stemming from the work on this project in Iceland and elsewhere. 

All the publications and software tools resulting from the project work are, and will remain, available in open access form at http://icetcs.ru.is/theofomon/, where further information about the project and its activities may be found.

Heiti verkefnis: TheoFoMon: Fræðileg undirstaða fyrir vöktun og sannprófun á keyrslutíma/ TheoFoMon: Theoretical Foundations for Monitorability
Verkefnisstjóri: Luca Aceto, Háskólanum í Reykjavík
Tegund styrks: Verkefnisstyrkur
Styrktímabil: 2016-2018
Fjárhæð styrks: 27,233 millj. kr. alls
Tilvísunarnúmer Rannís: 163406