Formale Methoden der Systemspezifikation Logische Spezifikation von Hard- und Software
description
Transcript of Formale Methoden der Systemspezifikation Logische Spezifikation von Hard- und Software
15.4.2008
Formale Methoden der SystemspezifikationLogische Spezifikation von Hard- und Software
Prof. Dr. Holger SchlingloffInstitut für Informatik der Humboldt Universität
und
Fraunhofer Institut für Rechnerarchitektur und Softwaretechnik
15.4.2008 Folie 2H. Schlingloff, Logische Spezifikation
Aufbau der Veranstaltung
1. Blockkurs „Algebraische Spezifikation von Software und Hardware“
Dr. Markus Roggenbach, Univ. Swansea voraussichtlich 23.-25.5. und 30.5.-1.6.2008 (n.V.) wie im SS2007 (VL & Ü)
2. Vorlesung (2SWS) „Logische Spezifikation“ diese Veranstaltung
3. Übungsaufgaben zur VL Dipl. Inf. Jan Calta, CZ Bearbeitung zum Bestehen der Prüfung essentiell
15.4.2008 Folie 3H. Schlingloff, Logische Spezifikation
Lernziele
• Kenntnisse über formale Spezifikationsmethoden zur Festlegung der Funktion von Systemen Historische Entwicklung, Stärken/Schwächen,
Möglichkeiten und Grenzen
• Fähigkeiten, diese für praktische Anwendungen einsetzen zu können Spielbeispiele / realistische Systeme industrielles Interesse (vgl. IEC61508)
• Umgang mit formalen Werkzeugen Checker, Prover, Transformatoren, …
15.4.2008 Folie 4H. Schlingloff, Logische Spezifikation
Einordnung
• praktische Informatik Spezifikation ist Teil der Systementwicklung Bezug zur theoretischer Informatik
• Verwandtes Modul: „Methoden und Modelle des Systementwurfs“ (W. Reisig) Fokus: hier Spezifikation, dort Modellierung fließende Übergänge, aber kaum Überlappung Methodenwissen ähnlich
• Weitere Bezüge Modellbasierte Softwareentwicklung (J. Fischer) Logik, Spiele und Automaten (M. Grohe) …
15.4.2008 Folie 5H. Schlingloff, Logische Spezifikation
weitere Ankündigungen
•Einschreibung in GOYA?
•Studien- und Diplomarbeiten
• Jobs bei FIRST
•Sokrates-Austausch mit UWales@Swansea
•Folien in Englisch?
15.4.2008 Folie 6H. Schlingloff, Logische Spezifikation
Definition of Terms
• System = „something composed“, i.e., everything here only: computational system (SW/HW) computation = transformation or transport of
information
• Specification = written description of a system „species facere“, making something visible can be informal or formal (we consider formal specs
only)
• Formal = in a certain fixed appearance syntax, semantics, derivation
• Logic = principles of reasoning logos = word, thought, reason „logic“ can also denote a certain formal language
15.4.2008 Folie 7H. Schlingloff, Logische Spezifikation
Specification of Systems
•Should be one of the first activities in software development requirements specification modelling
module decomposition implementation integration deployment
•Often neglected, mostly only informal
•Quality problems, acceptance problems
•Specification „a posteriori“
15.4.2008 Folie 8H. Schlingloff, Logische Spezifikation
Motivation
FIRST: “Understanding and mastering complex systems”
Examples: a video camera a car control unit a banking machine system a mobile phone communication protocol a fault tolerant computer for routing of trains an aircraft mission management system
• Understanding:Being able to describe what these systems are supposed to do
• Mastering:Being able to check whether they do what they are supposed
to do
Understanding and mastering human behaviour?
15.4.2008 Folie 9H. Schlingloff, Logische Spezifikation
A first example
A new video camcorder (“DCR-PC330”) owner's manual almost incomprehensible can be found in the internet typical for such devices
• Multifunctional on-off switch: up: off down: cycles through "tape", "memory" and "play/edit"
mode
• Intuitively, tape mode is for video, memory mode for pictures and play mode for viewing recorded material
15.4.2008 Folie 10H. Schlingloff, Logische Spezifikation
• How can we formally describe the behaviour of this switch? (Natural language description is ambivalent: What does "cycle"
mean? What if I push dn-dn-up-dn?)
• Modelling by finite transition system:
• States: {off, tape, memory, play}• Transition relations: {up, dn}
Transition system
off
memorytape play
dn
dn dn
dn
up up up
15.4.2008 Folie 11H. Schlingloff, Logische Spezifikation
•An alternative way to describe this switch: modal theory (description logic T-Box)
(For experts: additional axioms necessary, such as nondeterminism p -> []p)(For nonexperts: I assume you know about propositional logic)
Hybrid logic
tape dn memory up offmemory dn play up offplay dn tape up offoff dn tape [up] false
15.4.2008 Folie 12H. Schlingloff, Logische Spezifikation
Classical modal logic does not allow the use of state names.• Boolean properties describing the states:
(For experts: additional axioms necessary to inhibit impossible states)
(For the experts: this is a boolean encoding with three propositions.In principle, two would be enough, since on rec dv )
Modal logic
{tape, memory, play}||- on off||- on /* on = powered */ {tape, memory}||- rec {play, off}||- rec /* rec = can record */{tape, play}||- dv {memory, off}||- dv /* dv = head spinning */
off ||- on rec dv tape ||- on rec dv memory ||- on rec dv play ||- on rec dv
15.4.2008 Folie 13H. Schlingloff, Logische Spezifikation
Signature: P={on, rec, dv}, R={up, dn}Language:
Some valid properties: rec dv on on [up] on on dn on dv dn (dv dn dv)
15.4.2008 Folie 14H. Schlingloff, Logische Spezifikation
• Unique description of the behaviour of this switch!?
• Questions I might ask: in which state is the camcorder if I push dn-dn-up-dn? dndnupdn tape or dndnupdn (dv rec) can I always switch it off? up on how long will it stay on if I don't?
• In practice, no spec is ever complete! power failure while on shuts system off, power resume
brings it to “tape" mode
15.4.2008 Folie 15H. Schlingloff, Logische Spezifikation
• to model power failures, we have to distinguish between the state of the button (but_hi, but_lo) and the state of the camcorder (off, tape,...)
offbut_hi
memorytape play
dn
dn dn
dn
up up up
offbut_lo
pwr_fail
pwr_resume
15.4.2008 Folie 16H. Schlingloff, Logische Spezifikation
• Every model abstracts from details (e.g., there is a little green button within the switch which
arrests it in the "off" position)• A model is a means of communication between
humans (designers, users, ...) • Structuring the model as parallel hierarchical
transition system gives a statechart / state machine diagram
but_hi
but_lo
dn up
off
on
dn,pwr_res
up,pwr_fail
memorytape
play
dn
dn dn
onswitch camera
dn
15.4.2008 Folie 17H. Schlingloff, Logische Spezifikation
• Such models can help in the development of complex systems ("model-driven design")
• The more concrete the formalism, the closer it is to an implementation executable code may be generated from state
diagrams We might add additional information such as
timing, communication, variables and such.
• Specification as opposed to modeling describes properties of the targeted system not aiming at a complete description of the system not aiming at the generation of executable code