CS 599
Formal Methods in Software Architectures

Fall Semester, 2000
Location: WPH 106
Time: Th 2:00 - 4:50 pm
Class number: 048-33637D
Prerequisite: CS 612 or instructor’s consent


Instructor | OverviewReadingsAssignmentsSchedule


Instructor


Overview

Software architectures have gained a lot of popularity in the academic and commercial worlds during the last decade.  Numerous potential benefits have been attributed to architectures: ability to readily ensure system properties; improved support for software reuse; development of reliable, distributed, large-scale systems on time and within budget; and so forth.  In order to ensure these benefits, researchers have developed a set of modeling notations that allow architects to precisely specify the structure, behavior, and properties of the critical aspects of a system.  The precision of architectural models stems directly from each notation's underlying semantics, which is, in turn, based on a formal specification method (e.g., communicating sequential processes, Π calculus, finite state machines, temporal logic).

This course will expose students to formal specification methods, with a particular focus on those used in software architectures. A secondary focus of the class will be on the many software development activities, including architecture, that benefit from the use of formal methods. Several categories of formal methods will be studied, including algebraic, axiomatic, model-based, state-based, and temporal.  Specific modeling formalisms within each category will be highlighted and their applicability to software architectures assessed.  Students will study different types of formal specification languages and utilize specific languages to describe software systems. Students will demonstrate their understanding of the covered material through class presentations.  Additionally, students will be required to complete a course project that will investigate the application of a formal method on a specific, architecturally relevant problem.

At the end of the course, students should be conversant with the primary current approaches to formal methods and their use in software engineering. Students should be familiar with the “canonical” examples typically used in research papers (e.g., gas station, elevator, cruise control, alarm clock). Students should also be aware of the major open problems in the use of formal methods in software engineering and software architectures, such that research within this domain would be a natural follow-on to this course.

Course requirements are

[1]   reading relevant papers on formal methods,

[2]   a presentation of the details of one and a modeling exercise involving another formal method,

[3]   participation in class discussions, and

[4]   a semester project.


Readings


Assignments

Name

Description

Weight

Presentations 

Each student will be required to collaborate with one or two classmates and present the details of one category of formal methods.

25%

Examples

Each student will be require to collaborate with one or two classmates and model two example systems in a specific formal method (e.g., Statecharts or OBJ). The two examples are cruise control and gas station.

25%

Class participation

Students are expected to prepare for each class (by reading papers) and actively participate in the discussions of the topics for which they are not presenters.

25%

Class project

Eight groups of two students will use a single formal approach to provide an in-depth model of NeoChiron and, based on the primitives provided by NeoChiron, the C2 architectural style. NeoChiron has been referred to as the “assembly language” or architectural modeling and composition. The C2 style has a set of higher-order architectural primitives that should be expressible by an architectural “assembly language.” The students are required to select a formal method for which modeling and analysis tool support exists; each group is expected to analyze their model and demonstrate its properties. Given that different formal methods’ strengths and tool support vary, the demonstrated properties are also likely to be different across projects. Ultimately, the exercise will allow a comparison of the suitability of the various formal modeling techniques for the needs of software architectures and, potentially, the ability to combine them in a single specification. The details of the project are discussed and supporting materials provided in Week 4.

 

In addition to the 30-minute presentations of each project’s results, scheduled in class in weeks 14 and 15 of the semester, each group is also required to submit a detailed written report by December 11.

25%


Schedule (Subject to Change) 

Week

Date

Discussion Topic

Readings

Presenters

1

Aug 31

  • Course Introduction
  • Overview of Software Architectures (PDF)

 

  • Medvidovic

2

Sep 7

  • Introduction to Formal Methods (PDF)
  • Overview of Formal Methods in Software Architectures (PDF)
  • A. Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990.
  • R. A. Kemmerer. Integrating Formal Methods into the Development Process. IEEE Software, 7(5):37-50, September 1990.
  • J. M. Wing. A Specifier’s Introduction to Formal Methods. IEEE Computer, 23(9):8-24, September 1990.
  • N. Medvidovic and R. N. Taylor. A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering, 26(1):70-93, January 2000.
  • Medvidovic

3

Sep 14

DARPA meeting – No Class

4

Sep 21

  • Mehta and Medvidovic
  • D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8(1987):231-274, 1987.
  • J. M. Atlee and J. Gannon. State-Based Model Checking of Event-Driven System Requirements. IEEE Transactions on Software Engineering, 19(1):24-40, January 1993.
  • B. Auernheimer and R. A. Kemmerer. ASLAN User’s Manual. Technical Report TRCS84-10, University of California, Santa Barbara, April 1992.
  • B. Selic. Turning Clockwise: Using UML in the Real-Time Domain. Communications of the ACM, 42(10):46–54, October 1999.
  • Bhachech
  • Dincel
  • Mehta

5

Sep 28

 

  • Gao
  • Rakic
  • Roshandel
  • Axiomatic Specification (PDF)
  • C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10):576-583, October 1969.
  • D. C. Luckham and F. W. von Henke. An Overview of Anna, A Specification Language for Ada.  IEEE Software, 2(2):9-23, March 1985.
  • N. Medvidovic, D. S. Rosenblum, and R. N. Taylor. Heterogeneous Typing for Software Architectures. Submitted to ACM Transactions on Software Engineering and Methodology, 1999.
  • Al Said
  • Apcar
  • Jerejian

6

Oct 5

 

  • Dincel
  • Rampurwala
  • J. M. Spivey. The Z Notation: A Reference Manual. Oriel College, Oxford, England, 1998.
  • D. Jackson. Alloy: A Lightweight Object Modeling Notation. Technical Report, Laboratory of Computer Science, Massachusetts Institute of Technology, July 2000.
  • P. Inverardi and A. L. Wolf. Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model. IEEE Transactions on Software Engineering, 21(4):373-386, April 1995.
  • G. Abowd, R. Allen, and D. Garlan. Formalizing Style to Understand Descriptions of Software Architecture. ACM Transactions on Software Engineering and Methodology, October 1995.
  • T. Garg
  • Nagaraj

7

Oct 12

 

  • Mehta
  • Patel
  • Viswanathan
  • J. A. Goguen and T. Winkler. Introducing OBJ3. Technical Report, SRI-CSL-88-9, SRI International, August 1988.
  • J. V. Guttag, J. J. Horning, and J. M. Wing. The LARCH Family of Specification Languages. IEEE Software, 2(5):24-36, September 1985.
  • W. Tracz. Parameterized Programming in LILEANNA. ACM/SIGAPP Symposium on Applied Computing: States of the Art and Practice, Indianapolis, IN, February 1993.
  • Rakic
  • Roshandel

8

Oct 19

 

  • T. Garg
  • Nagaraj
  • L. Lamport. What Good Is Temporal Logic? 9th World Computer Congress, 657-668, Paris, France, IFIP, North Holland, 1992.
  • L. A. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith. Graphical Specifications for Concurrent Software Systems. 14th International Conference on Software Engineering, 214-224, May 1992.
  • D. C. Luckham, J. J. Kenney, L. M. Augustin, J. Vera, D. Bryan, and W. Mann. Specification and Analysis of System Architecture Using Rapide. IEEE Transactions on Software Engineering, 21(4):336-355, April 1995.
  • Patel
  • Viswanathan

9

Oct 26

 

  • U.A. Buy and R. Moll. A Specification-Based Approach to Concurrency Analysis. Journal of Automated Software Engineering, 2(2):265-309, 1995.
  • G. Naumovich, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil. Applying Static Analysis to Software Architectures. 6th European Software Engineering Conference together with 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 77-93, Zurich, Switzerland, September 1997.
  • R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, 6(3):213-249, July 1997.
  • A. Garg
  • Rampurwala

10

Nov 2

 

  • Apcar
  • Chiu
  • Jerejian
  • S. Igarashi, R. L. London, and D. C. Luckham. Automatic Program Verification I: A Logical Basis and Its Implementation. Acta Informatica, 4:145-182, 1975.
  • S. L. Hantler and J. C. King. An Introduction to Proving the Correctness of Programs. ACM Computing Surveys, 8(3):331-353, September 1976.
  • R. A. DeMillo, R. J. Lipton, and A. J. Perlis. Social Processes and Proofs of Theorems and Programs. Communications of the ACM, 22(5):271-280, May 1979.
  • M. Moriconi, X. Qian, and R. A. Riemenschneider. Correct Architecture Refinement. IEEE Transactions on Software Engineering, 21(4):356-372, April 1995.
  • Chiu
  • Gao

11

Nov 9

FSE 2000 – No Class

12

Nov 16

  • A. Finkelstein, D. Gabbay, A. Hunter, J. Kramer, and B. Nuseibeh. Inconsistency Handling in Multiperspective Specifications. IEEE Transactions on Software Engineering, 20(8):569-578, August 1994.
  • P. Zave and M. Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Transactions on Software Engineering, 22(7):508-528, July 1996.
  • L. Blair and G. Blair. Composition in Multi-Paradigm Specification Techniques. 3rd International Conference on Formal Methods for Open Object-Based Distributed Systems, Florence, Italy, February 15-18, 1999.
  • P. Tarr, H. Ossher, W. Harrison, and S. M. Sutton, Jr. N Degrees of Separation: Multi-Dimensional Separation of Concerns. 21st International Conference on Software Engineering, 107-119, Los Angeles, CA, May 1999.
  • Medvidovic

13

Nov 23

Thanksgiving Day – No Class

14

Nov 30

  • Project presentations and discussions

 

 

15

Dec 7

  • Project presentations and discussions

 

 

 

Dec 11

  • Final project write-ups due

 

 


Last updated:  11/16/00