View source

[[Forschungsbereich B|zum übergeordneten Forschungsbereich]]
===Verifikation selbstorganisierender Netze===
Bei häufigen Neukonfigurationen eines selbstorganisierenden Netzes sind auch die Zugriffsmöglichkeiten und Verfügbarkeiten dynamisch. Herkömmliche Verifikationsmöglichkeiten für Kommunikationsprotokolle sind für diesen Fall nur beschränkt einsetzbar. Zum einen ist der dynamische Aspekt der Ressourcenumverteilung nicht berücksichtigt, zum anderen beschränken sich die Methoden auf bestimmte Protokollebenen (z. B. Sicherungsschicht). Bei diesem Thema soll daher untersucht werden, inwieweit sich neuere logische und semantische Ansätze eignen, um die Protokolle selbstorganisierender Netze zu beschreiben und zu verifizieren. Konkrete Formalismen, die betrachtet werden sollen, sind hybride Logiken (HyLo) und abstrakte Zustandsmaschinen (ASMs). Hybride Logiken sind in der Expressivität zwischen der Aussagen- und der Prädikatenlogik angesiedelt; man hat die Möglichkeit, sowohl temporale Sachverhalte zu formalisieren als auch einzelne Objekte mit „nominals“ zu referenzieren. Damit wird es möglich, einzelne Kanäle logisch zu benennen und über ihre zeitliche Existenz zu argumentieren. Daher erscheinen diese Sprachen für den Kontext selbstorganisierender Netze besonders geeignet. Die Semantik dynamischer Systeme lässt sich mit abstrakten Zustandsmaschinen beschreiben. Ursprünglich wurden sie als Evolving Algebras zur Modellierung der Semantik temporaler Logiken konzipiert. Daher erscheinen sie auch als geeignet, die speziellen Anforderungen der Protokolle zur Selbstorganisation und ihrer hybriden Logiken zu modellieren. Forschungsthemen sind dabei einerseits die Modellierung selbst (im engen Zusammenhang mit den Vorhaben B2 und D3) und andererseits die abstrakte Semantik der verwendeten Logik. 
====Stand des Wissens====
Hybride modale und temporale Logiken wurden bereits in [1] definiert. Modelltheoretische Eigenschaften dieser Logiken wurden untersucht von Areces, deRijke und Blackburn, wobei [2] Beweisalgorithmen, Tableau und Sequenzkalküle untersucht. Seit Ende der 1980er Jahre werden ASM zur Beschreibung der Semantik von Programmiersprachen verwendet. In den letzten Jahren kamen weitere Anwendungen wie z.B. Kommunikationsprotokolle hinzu (siehe [3]). 
====Vorarbeiten der beteiligten Wissenschaftler====
[[Person:Schlingloff|H. Schlingloff]] beschäftigt sich seit langem mit Fragen der Spezifikation und Verifikation verteilter und kommunizierender Systeme. In [4] werden für die hier relevanten hybriden Modallogiken Expressivitäts- und Komplexitätsfragen untersucht und das Model-Checking-Problem beschrieben. Ausführliche Hintergrundinformationen zu Verifikationsansätzen als Ausgangspunkt für die geplanten Arbeiten sind in [5] zu finden. Eine neuere Anwendung auf den Bereich Web Services ist in [6] dargelegt und wird in einer Dissertation (D. Weinberg) weiter untersucht. Die Arbeit [7] behandelt die formale Spezifikation eines hochgradig sicherheitsrelevanten Protokolls für elektronische Bezahlsysteme. Auch diese Arbeiten werden in einer aktuellen Dissertation (S. Mishra) fortgeführt. Die Anwendung von modalen Logiken und der Theorie der Counterfactuals auf die modellbasierte Entwicklung sicherheitsrelevanter Bahncomputer wird in einer laufenden industriellen Dissertation (F. Lazos, Siemens Transportation Systems) untersucht. In [8] wird ein Überblick über den modellbasierten Entwicklungsprozess, so wie er heute im industriellen Umfeld diskutiert wird, gegeben. Die Arbeit [9] behandelt die Formalisierung informeller Anforderungsspezifikationen durch Modelle der UML als Erweiterung des modellbasierten Entwurfs im Bereich der Anforderungsanalyse. Ein Ansatz zur Formulierung des Korrektheitsbegriffs in Telekommunikationssystemen ist in [10] dargestellt. [[Person:Reisig|W. Reisig]] hat in [11] die Ausdrucksstärke und in [12] die genaue Beziehung zwischen Syntax und Semantik einer elementaren Klasse von ASM untersucht. In [13], [14] werden ASM zur Modellierung von Web Services verwendet. 
====Geplante Arbeiten====
In der geplanten Dissertation sollen die theoretischen Grundlagen für eine Verifikation selbstorganisierender Netze gelegt und auf die in den Forschungsbereichen [[Forschungsbereich A|A]] und [[Forschungsbereich C|C]] entwickelten Protokolle und Dienste angewendet werden. Insbesondere sollen dabei die Themen der Vorhaben [[Teilprojekt A1|A1]] und [[Teilprojekt A2|A2]] sowie [[Teilprojekt D1|D1]] als Motivation und Anwendungsfall für die zu untersuchenden Formalismen dienen. Es soll untersucht werden, welche Ausdrucksmittel eine hybride Modallogik bereitstellen muss, damit die relevanten Sicherheitsaspekte selbstorganisierender Netze ausgedrückt werden können. Dies geht einher mit einer exemplarischen Modellierung verschiedener Protokollebenen selbstorganisierender Netze. Auf der logischen Seite soll dann der Zusammenhang zu anderen Formalismen, wie z. B. TLA, und Multi-Agenten Logiken hergestellt und eine ASM-Semantik hybrider Logiken definiert werden. Auf der Anwendungsseite soll untersucht werden, wie Protokolle und Algorithmen abstrahiert werden können, damit die Korrektheit interaktiv beweisbar wird. Diese Verifikation soll an Beispielen exemplarisch durchgeführt werden. Daran schließen sich der Entwurf und die prototypische Implementierung von Entscheidungsverfahren sowie Verfahren für Simulation und Model-Checking von Kommunikationsprotokollen rekonfigurierbarer Netze an. Diese Verfahren sollen jeweils auf die konkreten Ergebnisse der Bereiche [[Forschungsbereich A|A]] und [[Forschungsbereich C|C]] angewendet werden.
====Referenzen====
'''[1]'''	A. Prior: Past, Present and Future. Oxford University Press, 1967. 

'''[2]'''	P. Blackburn: Representation, Reasoning, and Relational Structures- a Hybrid Logic Manifesto. In: Proc. of the 1st. Method for Modalities Workshop. Amsterdam. C. Areces, E. Franconi, R. Goré, M. de Rijke, H., Schlingloff (eds.) Special Issue of the Logic Journal of the IGPL. Vol 8:3, pp. 339-625, 2000. 

'''[3]'''	E. Boerger, R. Staerk: Abstract State Machines. Springer-Verlag 2003. 

'''[4]'''	M. Franceschet, M. deRijke, and H. Schlingloff: Hybrid Logics on Linear Structures- Expressivity and Complexity. In: TIME/ICTL 2003. 4th International Conference on Temporal Logic (July 2003). Cairns, Queensland, Australia. IEEE Computer Society Press, 2003. 

'''[5]'''	E. M. Clarke, H. Schlingloff: Model Checking. Chapter 21 in Alan Robinson and Andrei Voronkov (eds. ), Handbook of Automated Reasoning; Elsevier Science Publishers B. V., pp. 1367 – 1522, 2000. 

'''[6]'''	A. Martens, H. Schlingloff, K. Schmidt: Modeling and Model Checking Web Services. To appear in: ENTCS - Electronic Notes in Theoretical Computer Science; Elsevier, 2005. 

'''[7]'''	A. Gimblett, M. Roggenbach, and H. Schlingloff: Towards a formal specification of electronic payment systems in CSP-CASL. Selected papers from WADT 2004. 17th International Workshop on Algebraic Development Techniques, Barcelona, Spain. (March 2004). Springer LNCS 3423, pp. 61-78, 2005.

'''[8]'''	H. Schlingloff, C. Sühl, H. Dörr, M. Conrad, J. Stroop, S. Sadeghipour, M. Kühl, F. Rammig, G. Engels: Eine integrierte Methodik zur modellbasierten Steuergeräteentwicklung. In: BMBF-Workshop Software Engineering 2006 Berlin, July 2004. 

'''[9]'''	M. Friske, H. Schlingloff: Von Use Cases zu Test Cases- Eine systematische Vorgehensweise. In: MBEES - Model Based Engineering of Embedded Systems Dagstuhl (Dez. 2004). T. Klein, B. Rumpe, B. Schätz (eds.); TU Braunschweig Report TUBS-SSE 2005-01; VII, 2004. 

'''[10]'''	M. Frey, H. Schlingloff: Conformance of Distributed Systems. In: TestCom 2003 on Next Generation Testing for Next Generation Networks. 15th IFIP International Conference on Testing of Communicating Systems, Sophia Antipolis, France, May 26-28, 2003, Springer LNCS 2644, May 2003. 

'''[11]'''	W. Reisig: On a Theorem of Gurevich on the expressive power of elementary ASM. Acta Informatica, 2003. 

'''[12]'''	W. Reisig: The semantic kernel of ASM. Submitted for TCS, 2005. 

'''[13]'''	W. Reisig, A. Brade: ASM models for Web Services. Informatik-Berichte Nr. 181, Humboldt-Universität zu Berlin, 2004.
 
'''[14]'''	D. Fahland, W. Reisig: ASM based semantics for BPEL. The negative control flow International ASM Conference, Paris, März 2005.