Up
CSE291 Spring 2005
CSE218 Winter 2005
CSE291 Spring 2004
CSE218 Winter 2004
CSE218 Winter 2003
CSE 290

Overview

The need for highly dependable software systems continues to grow rapidly. Embedded within automobiles, aircraft, medical equipment, entertainment, household, and productivity devices, safety-critical systems have found their way into all facets of our daily lives. Advances in wired and wireless networking infrastructure enable an unprecedented degree of interconnection between previously separate functional entities. Increasingly, the resulting degree of complexity becomes the limiting factor for providing correct, safe and secure implementations of new applications, as well as for enhancing existing solutions by means of new features.

In this course we will study theory, methods and tools for establishing reliable software systems. In particular, we will visit the following topics:

General Information

Tentative Schedule of Topics

Grading

There will be no final exam. This class is seminar-style, with a strong reading component. The grade will be determined based on individual achievements and teamwork. Individual achievements are participation in classroom discussion, and at least three paper presentations in class. Project teamwork consists  of 2-3 students working together on some aspect of system verification (this can include composition, experimentation and enhancement of tools for software modeling and verification). This involves writing a project progress report (max. 5 pages), and a final project report (max. 20 pages) as a team effort. The details regarding the papers to read, and the project topics will be discussed during the first class meeting. Individual achievements and teamwork contribute as follows to the overall grade:

    35% Paper presentations
    15% Classroom participation
    50% Project

Literature

required:

Doron Peled: Software Reliability Methods. Springer, 2001

Further Reading

Additional texts, from which topics presented by students in class will be drawn, include:

1. Background

1. R. Alur, D.L. Dill. A Theory of Timed Automata. in: Theoretical Computer Science Vol. 126, No. 2, April 1994, pp. 183-236. http://citeseer.ist.psu.edu/alur94theory.html

2. Beeck, M. von der. A comparison of statecharts variants. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pages 128--148. Springer-Verlag, 1994.

3. Gregor Bochmann. Finite State Description of Communication Protocols. Computer Networks, 2:362-372, 1978

4. E.W. Dijkstra: Cooperating Sequential Processes. EWD 123
   http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD123.PDF 

5. R. Floyd: Assigning Meaning to Programs. In J. T. Schwartz (ed.):  Proceedings of Symposium on Applied Mathematical Aspects of Computer Science. American mathematical Society, 1967, 19-32.
   http://raw.cs.berkeley.edu/Papers/FloydMeaning.pdf

6. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231--274, 1987. http://citeseer.ist.psu.edu/harel87statecharts.html

7. C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10): 576-580 (1969)
   http://portal.acm.org/citation.cfm?doid=363235.363259

8. Gerard J. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991
   http://spinroot.com/spin/Doc/Book91.html

9. Gary Levin, David Gries: A Proof Technique for Communicating Sequential Processes. Acta Inf. 15: 281-302 (1981)

10. T. Nipkow. Term rewriting and beyond---theorem proving in Isabelle. Formal Aspects of Computing, 1:320--338, 1989

11. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319-340, 1976

12. D. Park. Concurrency and automata on infinite sequences. LNCS 104, pages 167--183, 1981

2. Safety and Liveness

1. B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117—126, 1987.
   http://citeseer.ist.psu.edu/alpern86recognizing.html

2. A.P. Sistla: Safety, Liveness, and Fairness in Temporal Logic. Formal Aspects of Computing 6(1994), 495—511
   http://citeseer.ist.psu.edu/prasadsistla99safety.html

3. Formal Models & Model Checking

1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In 38th Annual Symposium on Foundations of Computer Science, pages 100-109, Miami Beach, Florida, 20-22 October 1997
   http://citeseer.ist.psu.edu/alur97alternatingtime.html

2. M. Broy: Compositional Refinement of Interactive Systems, No. 89, Digital Systems Research Center, Palo Alto, California, July 1992.
   http://citeseer.ist.psu.edu/article/broy92compositional.html

3. Manfred Broy, Ingolf Krüger: Interaction Interfaces - Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts. ICFEM 1998
   http://www4.informatik.tu-muenchen.de/publ/papers/BK98.pdf

4. M.C. Browne, E.M. Clarke, O. Grumberg: Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59 (1,2), 1988, pp. 115-131.

5. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking 10²⁰ states and beyond. Information and Computation, 98(2):142--170, June 1992.
   http://citeseer.ist.psu.edu/burch90symbolic.html

6. K. M. Chandy and J. Misra: Proofs of Networks of Processes
   IEEE, Vol. SE-7, No. 4, pp. 417-426
   http://www.cs.utexas.edu/users/misra/scannedPdf.dir/ProofsNetworks.pdf

7. E. Allen Emerson, E. M. Clarke: Characterizing correctness properties of parallel programs using fixpoints. In Proceedings of the 7th International Colloquiurn on Automata, Languages, and Programming. Lectures Notes in Computer Science, vol. 85, Springer-Verlag, New York, 1980, pp. 169-181.

8. Emerson, E. A.: Automated temporal reasoning about reactive systems. In Logics for Concurrency: Structure versus Automata, number 1043 in Lecture Notes in Computer Science. Springer-Verlag. 41—101, 1996.
   http://citeseer.ist.psu.edu/emerson96automated.html

9. R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
   http://citeseer.ist.psu.edu/gerth95simple.html

10. Patrice Godefroid, Sarfraz Khurshid: Exploring Very Large State Spaces Using Genetic Algorithms, J.-P. Katoen and P. Stevens (Eds.): TACAS 2002, LNCS 2280, pp. 266–280, 2002.

11. Patrice Godefroid, Doron Peled, Mark G. Staskauskas: Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs. ISSTA 1996: 261-269
    http://portal.acm.org/citation.cfm?doid=229000.226324

12. Patrice Godefroid, Pierre Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2): 149-164 (1993)

13. Patrice Godefroid, Pierre Wolper: A Partial Approach to Model Checking. LICS 1991: 406-415

14. Patrice Godefroid: Using Partial Orders to Improve Automatic Verification Methods. CAV 1990: 176-185

15. Wilsin Gosti, Tiziano Villa, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli: An Exact Input Encoding Algorithm for BDDs Representing FSMs. In: Great Lakes Symposium on VLSI '98, IEEE, 1998

16. Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872 – 923, March 1994.
    http://citeseer.ist.psu.edu/lamport90temporal.html  

17. Manna, Z, and A. Pnueli. How to cook a temporal proof system for your pet language. Proc. of the Symposium on Principles of Programrning Languages, ACM, Austin, Jan. 1983
    http://doi.acm.org/10.1145/567067.567082

18. Markus Kaltenbach, Jayadev Misra: Formal Methods at the Crossroads: From Panacea to Foundational Support, ed. Bernhard K. Aichernig and Tom Maibaum, LNCS 2757, pp 423-438, Springer-Verlag, 2003
    http://www.cs.utexas.edu/users/psp/hmc.pdf

19. Jayadev Misra: A Simple, Object-based View of Multiprogramming,
    Formal Methods in System Design, Vol. 20, No. 1, January 2002
    http://www.cs.utexas.edu/users/psp/ModularMultiprog.pdf

20. Jayadev Misra: A logic for Concurrent Programming (in two parts): Safety and Progress,
    Journal of Computer and Software Engineering, Vol.3, No.2, pp 239-300, 1995
    http://www.cs.utexas.edu/users/psp/SafetyProgress.pdf

21. Jayadev Misra: Loosely Coupled Processes, Future Generations Computer Systems 8, 269-286, North-Holland, 1992
    http://www.cs.utexas.edu/users/psp/loosely-coupled.pdf

22. Doron Peled, Amir Pnueli: Proving Partial Order Properties. TCS 126(2): 143-182 (1994)

23. A Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, 1977

24. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, volume 137 of Lecture Notes in Computer Science, pages 337--351. Springer, 1982

25. S. Safra. On the complexity of omega-automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS'88, pages 319--327, Los Alamitos, California, October 1988. IEEE Computer Society Press

26. Sistla, A. P., Clarke, E. M., Francez, N., and Meyer, A. R., Can Message Buffers be Axiomatized in Temporal Logic?, Information & Control, vol. 63., nos. 1/2, Oct./Nov. 84, pp. 88-112.

27. Moshe Y. Vardi, Pierre Wolper: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). LICS 1986: 332-344

28. Pierre Wolper: Expressing Interesting Properties of Programs in Propositional Temporal Logic. POPL 1986: 184-193

29.  

4. Real-Time Systems

1. M. Abadi and L. Lamport. An Old-Fashioned Recipe for Real Time. In Proc. of REX Workshop "Real-Time: Theory in Practice", volume 600 of Lecture Notes in Computer Science, 1993.
   http://citeseer.ist.psu.edu/article/abadi93oldfashioned.html

5. Synthesis

1. Haghverdi E. and Ural H.: Submodule Construction from Concurrent System Specifications. Information and Software Technology, (41) 8, 1999, pp. 499-506,
   http://citeseer.ist.psu.edu/haghverdi98submodule.html

2. I. Krüger, R. Grosu, P. Scholz, M. Broy: From MSCs to Statecharts, in: Franz J. Rammig (ed.): Distributed and Parallel Embedded Systems, Kluwer Academic Publishers, 1999
   http://www4.informatik.tu-muenchen.de/publ/html.php?e=254

3. S. Uchitel, J. Kramer, J. Magee: Synthesis of Behavioral Models from Scenarios. IEEE Transactions on Software Engineering, Vol. 29, Issue 2, Pages: 99 - 115, 2003
   http://csdl.computer.org/comp/trans/ts/2003/02/e0099abs.htm

6. Testing

1. Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, and Bernhard Steffen: On the Correspondence Between Conformance Testing and Regular Inference. In: M. Cerioli (Ed.): FASE 2005, LNCS 3442, pp. 175–189, 2005.

2. Anders Ek, Jens Grabowski, Dieter Hogrefe, Richard Jerome, Beat Koch, Michael Schmitt II: Towards the industrial use of validation techniques and automatic test generation methods for SDL specifications. SDL Forum 1997: 245-260

3. Elsa L. Gunter, Doron Peled: Using Functional Languages in Formal Methods: The PET System . PDPTA 2000: 2981-2986
   http://www.dcs.warwick.ac.uk/~doron/dblp.html

4. Elsa L. Gunter, Robert P. Kurshan, Doron Peled: PET: An Interactive Software Testing Tool. CAV 2000: 552-556
   http://www.dcs.warwick.ac.uk/~doron/dblp.html

5. Elsa L. Gunter, Doron Peled: Path Exploration Tool. TACAS 1999: 405-419
   http://www.dcs.warwick.ac.uk/~doron/dblp.html

6. Hardi Hungar, Tiziana Margaria, Bernhard Steffen: Test-based Model Generation for Legacy Systems. In: Proceedings of the International Test Conference 2003, 2003

7. Therese Berg1, Olga Grinchtein1, Bengt Jonsson1, Martin Leucker2, Harald Raffelt3, and Bernhard Steffen3: Domain-Specific Optimization in Automata Learning. In:

8. D. Lee and M. Yannakakis, Principles and methods of testing finite state machines - a survey, Proc. of the IEEE, vol. 84, pp. 1090--1123, Aug 1996.
   http://citeseer.ist.psu.edu/lee96principles.html

9. N. Sharygina and D. Peled. A Combined Testing and Verification Approach for Software Reliability. In Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, pages 611-628, 2001
   http://www.dcs.warwick.ac.uk/~doron/dblp.html

7. Tools

1. SPIN: http://spinroot.com/spin/whatispin.html

2. SMV: http://www-2.cs.cmu.edu/~modelcheck/smv.html

3. NuSMV: http://sra.itc.it/tools/nusmv/index.html

4. Cadence SMV: http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/

5. BMC: http://www-2.cs.cmu.edu/~modelcheck/bmc.html

6. Murphi: http://verify.stanford.edu/dill/murphi.html

7. CADP: http://www.inrialpes.fr/vasy/cadp.html#Language

8. PEP: http://theoretica.informatik.uni-oldenburg.de/~pep/

9. Java Pathfinder: http://ase.arc.nasa.gov/havelund/jpf.html

10. Bandera: http://bandera.projects.cis.ksu.edu/

11. JCAT: http://www.dai-arc.polito.it/dai-arc/auto/tools/tool6.shtml

12. Java Model Checker: http://sprout.stanford.edu/uli/

13. UV System: http://www.cs.utexas.edu/users/psp/markus/uv2/welcome.html

14. Ptolemy II: http://ptolemy.eecs.berkeley.edu/ptolemyII/

15. AutoFocus: http://autofocus.in.tum.de/index-e.html

Initial version: March 28, 2005, by Ingolf Krueger