Preliminär Disposition

Under introduktionsföreläsningen ska vi hitta två gemensamma dubbeltimmar i undervisningsveckan(dvs v11-13 och v17-20). Den första för föreläsning och diskussion om teoristoffet (hålls till minsta möjliga) och den andra för diskussionsseminarier. Reviderat schema med aktuell kursadministration.

Förslag: Må 13-15 Föreläsning, Fr 10-12 Redovisning/diskussion under Må 11 mars - fr 29 mars, må 22 april - fr 10 maj. OBS: till fredagstiden bör alla som avser att få poäng för kursen ha läst de artiklar som ska gås igenom.

1F Må 11/3     Introduktion/översikt, Historik. Floyd-Hoare-
  	         metoden. Välgrundade mängder och avslutning. 
1R Fr 15/3     Modellbaserad notation, Z  och Morgan/Dijkstras
                 notation. Förfining. Kod som specialfall av
                 specifikation. Utdelning av hemuppgift 1.
2F Må 18/3     Första ordningens språk. Ekvationer och 
                 omskrivning. Axiom, hypoteser, mekaniserade 
                 bevis. Knuth-Bendix metod.
2R Fr 22/3    Diskussion av Hoare-Wirth, Parnas, Parnas et al.
3F Må 25/3    Larch: LSL/LCL, LP, LCLint. (Inlämning av 
               hemuppgift 1, utdelning av uppgift 2)
3R Fr 29/3    Diskussion av Rosenblum, Sommerville Ch 8, Ch 9,
               Jacky.
4F Må 22/4    Gästföreläsare (industriorienterat)
4R Fr 26/4    Diskussion av Broy, Broy, Wing.
5F Må 29/4    MS- och temporallogiker. Automater på oändliga
  	         strängar och träd. Modellverifiering.
5R Fr 3/5     Diskussion av Ciaccia, Ciaccia, Clarke et al.
6F Må 6/5     Tekniska system med programvara och maskinvara.
                 Markovmodellering
6R Fr 10/5    Diskussion av Klarlund et al, Johnson-Butler.
7F Må 13/5    Realisering av verifieringsmetodik. (Inlämning av 
                 hemuppgift 2).
7R EÖ         Diskussion av Rosenbaum, Musa. Avslutning.

Litteratur.

Carroll Morgan: Programming from specifications, Prentice-Hall 1994, ISBN 0-13-123274-6. Denna bok har fått mycket goda recensioner och är idag den bästa läroboken på grundnivå. För finsmakare kan Dijkstras 'A discipline of Programming' vara ett alternativ(se nedan). Den har dock rapporterats vara krävande även som doktorandkursbok (jag håller inte riktigt med om detta, däremot är den mycket gammal).

Samt en handfull artiklar/bokkapitel som illustrerar olika perspektiv och metoder på området:

Hoare, Wirth: An axiomatic definition of the programming language pascal, Acta Informatica 2(1973), 235-355
D.Parnas: Teaching Programming as Engineering, LNCS 967
D.Parnas, Madey and Iglewski: Precise Documentation of Well-structured programs, IEEE Trans Software Engineering, 20(12) 1994, 948-976.
D. Rosenblum: A practical approach to programming with assertions. IEEE Tr Software Engineering, 21(1995) 19-31.
Sommerville: Software Engineering Ch 8 , Ch 9.
J Jacky: Specifying a safety-critical control system in Z, IEEE Tr Software Engineering, 21(1995) 99-105.
Jeanette Wing: Hints to Specifiers. CMU-CS-95-118R
D Evans, John Guttag, James Horning, Yang Meng Tan: LCLint: A tool for using specifications to check code.
M. Broy: Experiences with Software Specification and verification using LP, the Larch proof assistant. DEC Systems Reearch Center, 93, Nov 1992
P.Ciaccia, P. Ciancarini, W. Penzo: A formal approach to software design: the Clepsydra methodology.
P.Ciaccia, P. Ciancarini: A course on Formal methods in software engineering: Matching requirements with design. LNCS967.
R. Allen, D. Garlan: Formal Connectors, CMU-CS-94-115.
Arnborg, S., Decomposable structures, Boolean function representations, and optimization, MFCS 1995, LNCS 969, 21-36.
(UTGAR) W.Thomas: Automata on infinite objects, Handbook of TCS
E.Clarke, D.Grumberg, D.Long: Model Checking and abstraction, ACM Tr Programming Languages and Systems, 16(5)1994, 1512-1542.
D Basin, N. Klarlund: Hardware verification using Monadic Second Order Logic. BRICS report RS-95-7 (1995).
Sally Johnsson, Ricky Butler: Design for validation, 10th Digital Avionics Systems Conf., 1991;
R Butler, S Johnsson: Techniques for modelling the reliability of fault-tolerant systems with the markov state-space approach. NASA Reference Publication 1348, 1995.
A.Somani, J.A. Ritcey, S.H.L. Au: Computationally efficient phased mission reliability analysis for systems with variable configurations. IEEE Tr on Reliability, 41(4), Dec 1992 504-511.
John D. Musa: Software reliability engineering, University Video Communications and IEEE Software 1993.
Suzanne Rosenbaum: How to improve software engineering practices, IEEE ICSE 1993, och University Video Communications.

Och manualer för programsystemen som används i labbarna (preliminärt):
- Arnborg: MS tool users guide (eller Klarlund: MONA Users guide.)
Några resurspekare på Internet:
Newsgrupper:
- comp.specification.z
- comp.specification.larch
- comp.specification.misc
Intressant övrig litteratur:
- N. Francez: Program Verification. Addison-Wesley 1992 ISBN 0-201-41608-5
- Guttag, John and Horning, James: Larch: Languages and Tools for Formal Specification, Springer-Verlag,1993
- E. Dijkstra: A Discipline of Programming,Prentice-Hall 1976. ISBN 0-130215871-X

Liknande Kurser

2G1301: Teori för distribuerade system
Models of Software systems
Methods of Software development
Björn Lispers planerade semantikkurs

Ingång till Nadas kursweb

Stefan