Drittmittelprojekt: Formale Spezifikation des LCAS-Protokolls mit SpecEdit
Inhalt
Im Projekt wurde LCAS (Link Capacity Adjustment Scheme), ein Protokoll, daß bei der dynamischen Bandbreitenanpassung in den Weitverkehrsnetzen der synchronen digitalen Hierarchie (SDH) Verwendung findet, formal spezifiziert. Den Ausgangspunkt hierfür bildete eine textuelle Spezifikation, die unter Zuhilfenahme von SpecEdit, einem Werkzeug zur formalen Spezifikationserfassung, in eine formale und damit prüfbare Beschreibung umgesetzt wurde. Ziel des Projektes war einerseits, Inkonsistenzen und Mehrdeutigkeiten in der zugrunde liegenden Spezifikation aufzudecken, andererseits die Eignung von SpecEdit zur Modellierung eines solch komplexen Systems nachzuweisen.
Ergebnisse
- Formale Spezifikation des LCAS-Protokolls auf Basis einer vorgegebenen textuellen Spezifikation
- Nachweis von Mehrdeutigkeiten und Inkonsistenzen in der vorgegebenen Spezifikation
- Verifikation der von SpecEdit generierten VHDL-Modellbeschreibung anhand einer VHDL-Testbench
Kooperationspartner
- Lucent Technologies, Nürnberg
Tags
Laufzeit
May 2005
July 2005
