Distribuerede og Indlejrede Systemer (DES) tidligere DSS
Enhedens forskning omhandler modellering, analyse og implementering af computer programmer med fokus på distribuerede og indlejrede systemer. Forskningen inkluderer følgende områder:
- Semantiske teorier til modellering af computer programmer og systemers adfærd.
- Design, implementering og modeller til analyse af distribuerede systemer og netværk.
- Algoritmer, metoder og værktøjer til verifikation og validering af programmer og systemer.
Distribuerede og Indlejrede systemer enheden blev dannet i dens nuværende form i 1997 ved en fusion af to tidligere forskningsenheder indenfor Datamatiske Systemer og Formelle Systemer. Enheden har siden 1993 sammen med kolleger fra Århus Universitet været en del af BRICS, et grundforskningscenter i datalogi (eng.: "Center for Basic Research in Computer Science"). Enheden valgte i marts 2008 at ændre navnet til Distribuerede og Indlejrede Systemer (DES).
Center for Indlejrede Software Systemer (CISS) blev etableret i 2001 i et samarbejde med Institut for Elektroniske Systemer ved Aalborg Universitet. Målet for CISS er at fungere som et industri-rettet forskningscenter af største excellence med en klar og synlig profil inden for software konstruktion og indlejrede systemer, som både udnytter enhedens eksisterende forskning, og inspirerer til ny forskning. Enhedens forskning spænder derfor vidt, fra udvikling af det semantiske fundament for computer beregning og parallelitet (eng.: concurrency), til bidrag til den nyeste teknologi inden for indlejrede, sandtids, og netværksbaserede systemer. Det er en stor udfordring at producere forskning af høj kvalitet i et sådant bredt fagligt spektrum, men den fælles interesse for distribuerede og parallelle systemer giver enhedens aktiviteter et sammenhængende fokus.
De ovenstående tre forskningsområder udgør hver især et selvstændigt emne, men er også indbyrdes afhængige på et utal måder: semantiske modeller giver vigtige anvisninger på hvad sprog og paradigmer til distribuerede systemer skal indeholde, og hvordan de opbygges; semantiske modeller er en forudsætning for udvikling af verifikationsalgoritmer og værktøjer; udvikling af valideringsværktøjer giver både ny indsigt i de anvendte underliggende semantiske modeller, og anvendes i udviklingsomgivelser til konstruktion og analyse af distribuerede systemer; det faktum at da distribuerede systemer til stadighed ændrer karakter og udvikler sig giver de indsigt i eksisterende semantiske modellers styrker og svagheder; endeligt så udstiller distribuerede systemer begrænsningerne ved de givne verifikationsalgoritmer og værktøjer.
Enhedens nuværende forskning inkluderer de følgende aktiviteter:
- Teorier for parallelitet: Semantiske teorier og meta-teorier for parallelle processer og deres logiske egenskaber. Semantiske teorier for processer med dynamisk kommunikations-topologi, herunder sikkerhedsprotokoller. Studie af nye udvidelser, som fx. hybride, sandtids, og probabilistiske processer.
- Verifikation and Validering: Udvikling og implementation af data strukturer, algoritmer og værktøjer til model-checking af indlejrede og sandtidssystemer. Anvendelse på kommunikationsprotokoller, kontrol programmer, og planlægning og afvikling.
- Indlejrede Systemer: Metoder til specifikation, analyse og test af indlejrede systemer. Modellering og analyse af industrielle eksempel-systemer. Teoretisk fundament for indlejrede og hybride systemer.
- Netværk og Operativ Systemer: Analyse og konstruktion af services og protokoller til computer netværk, herunder grid-beregning og parallel-beregning med stor ydelse. Operativ systemer til indlejrede og sandtidssystemer.