course_outline
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| course_outline [2012/09/14 01:46] – jonathan | course_outline [2012/11/28 19:55] (current) – jonathan | ||
|---|---|---|---|
| Line 13: | Line 13: | ||
| ===== Tabular expressions ===== | ===== Tabular expressions ===== | ||
| - | * See 03 (Parnas function tables/ | ||
| * Tabular expressions help to provide complete and disjoint specifications | * Tabular expressions help to provide complete and disjoint specifications | ||
| - | * Tabular expressions help to develop test cases | + | * Tabular expressions help to develop test cases. They cover all the corner cases. |
| + | * Why will tabular expressions help developers produce better code? | ||
| + | * What does it mean for a tabular expression to be well-defined? | ||
| + | * See slides 03 (Parnas function tables/ | ||
| *** Required readings**: Slides 1-15 of '' | *** Required readings**: Slides 1-15 of '' | ||
| ===== Context diagrams and R/ | ===== Context diagrams and R/ | ||
| * Context diagrams. Why do we need them? What are monitored and what are controlled variables? | * Context diagrams. Why do we need them? What are monitored and what are controlled variables? | ||
| + | * What are the phenomena of the environment? | ||
| * What is the difference between a R-description and an E-description? | * What is the difference between a R-description and an E-description? | ||
| * See 04 slides on leap years, date validation and birthday book for examples of context diagrams and R/E descriptions. | * See 04 slides on leap years, date validation and birthday book for examples of context diagrams and R/E descriptions. | ||
| + | * To code we need requirements To write requirements we need domain knowledge. What is domain knowledge? | ||
| * **Required reading**: How to write requirements (Telelogic), | * **Required reading**: How to write requirements (Telelogic), | ||
| - | ===== Mathematical specification modules | + | ===== MSR - Module specifications for reactive and transformational systems |
| + | |||
| + | MSR uses a combination of ideas from Z, B, Event-B and Parnas function tables for the mathematical specification of systems. The suggested text uses Z for part of the course. | ||
| * What are specification modules? How do they differ from design modules or code modules? | * What are specification modules? How do they differ from design modules or code modules? | ||
| * Review of predicate logic, set theory, functions (total, partial, injective, surjective, bijective), relations, sequences, bags. | * Review of predicate logic, set theory, functions (total, partial, injective, surjective, bijective), relations, sequences, bags. | ||
| Line 39: | Line 46: | ||
| * Note that a precise and complete mathematical specification of the birthday book (specification modules and tabular expression) is less than two pages. The specification describes precise outputs for all possible inputs whether valid or invalid. The specification can be used to predict the future behaviour of any software machine that implements the specification. | * Note that a precise and complete mathematical specification of the birthday book (specification modules and tabular expression) is less than two pages. The specification describes precise outputs for all possible inputs whether valid or invalid. The specification can be used to predict the future behaviour of any software machine that implements the specification. | ||
| + | ===== Requirements for the Dell Keyboard ===== | ||
| + | |||
| + | We discuss the paper by Baber, Parnas and Vilkomer (it is in Slides/ | ||
| + | |||
| + | Abstract: We describe our experience applying tabular | ||
| + | mathematical approaches to software specifications. | ||
| + | Our purpose is to show alternative approaches to | ||
| + | writing tabular specifications and to help practitioners | ||
| + | who want to apply such methods by allowing | ||
| + | them to pick the best one for their problem. | ||
| + | The object for the case study is software used by | ||
| + | Dell Products for testing the functionality of the keyboards | ||
| + | on notebook computers. Starting from informal | ||
| + | documents, we developed a variety of tabular representations | ||
| + | of finite state machine specifications and | ||
| + | tabular trace specifications. We found that the discipline | ||
| + | required by these methods raised issues that had | ||
| + | never been considered and resulted in documents that | ||
| + | were both more complete and much clearer. The various | ||
| + | tabular representations are compared from a | ||
| + | user’s point of view, i.e., clarity, consistency, | ||
| + | completeness, | ||
| + | Keywords: software, tabular specifications, | ||
| + | state machine, traces, trace specifications. | ||
| + | |||
| + | Required: Watch a [[http:// | ||
| + | |||
| + | ===== UML for Requirements ===== | ||
| + | |||
| + | The suggested text discusses how UML models are used in requirements engineering. We discuss use cases/ | ||
| + | |||
| + | ===== Writing requirements for reactive/ | ||
| + | * Difference between transformational and reactive systems | ||
| + | * Safety critical systems are usually reactive | ||
| + | * Difference between proof systems and model checking | ||
| + | * Timed Transition Models | ||
| + | * types, constants and variables | ||
| + | * module templates with in, out and share variables | ||
| + | * module instants | ||
| + | * module compositions | ||
| + | * model-checking and reachability graphs | ||
| + | * temporal logic specifications | ||
| + | * safety properties and liveness properties | ||
| + | * discussion of the the bridge controller | ||
| + | |||
| + | ===== General Considerations ===== | ||
| + | |||
| + | This is covered in the slides in the SVN: Readings/ | ||
course_outline.1347587195.txt.gz · Last modified: 2012/09/14 01:46 by jonathan