Formal Specification and Design Techniques

An example of informal specification

• A software system for an Automated Teller

Machine (ATM) needs to provide services on

various accounts.

• The services include

operations on current account, operations on

savings account, transferring money between

accounts, managing foreign currency account,

and change password.

• The operations on a current or savings account include deposit, withdraw, show balance, and print out

transaction records.

Problems with informal specification

• Informal specifications are likely to be ambiguous, which is likely to cause miss-interpretations.
• Informal specifications are difficult to be used for testing of programs, program specifications and the program structures.
• Informal specifications are difficult to be analyzed for their consistency and validity.
• Information specifications are difficult to be supported by software tools in their analysis, transformation, and management (e.g., search, change, reuse).

Better way to write the same specification

Operations

• deposit
• withdraw
• show balance
• print out transaction records.

Services

• operations on current account
• operations on savings account
• transferring money between accounts
• managing foreign currency account,
• change password.

Advantages of block diagrams and flow charts

• The parties understand each other more rapidly and better in discussions, since they always had a picture of what the other meant and what he was talking about.
• Specifications and documentations are easier to read, less tiring and, more easily understandable.
• Meetings with users may be more pleasant and more effective, since the diagrams at least enables them to imagine what the systems analysts are getting at with their flowcharts.
• Difficulties in communication is still existed between users and system designers. However, they are less problematic and less time-consuming.

Shortcomings of flow charts and block diagrams (informal specification)

• They are unstructured and many computer scientists also tended to reject anything that looked faintly like a flowchart.
• They had neither syntax nor semantics.
• It is impossible to prove their formal correctness of the model of system.
• Difficult to establish precise mapping rules to "transform" a specification into an algorithm or verify a program section.

Refinement

Specification

Implementation

Verification

What to do

Check the correctness

How to do it

Testing

Requirements analysis

Design (modeling)

Coding

Formal Specification

Verification

Verification

Validation

Diagram	Description
Class	Represents the object orientation of a system. Shows how classes are statically related.
Object	Represents a set of objects and their relationships at runtime and also represent the static view of the system.
Component	Describes all the components, their interrelationship, interactions and interface of the system.
Composite structure	Describes inner structure of component including all classes, interfaces of the component, etc.
Package	Describes the package structure and organization. Covers classes in the package and packages within another package.
Deployment	Deployment diagrams are a set of nodes and their relationships. These nodes are physical entities where the components are deployed.

Diagram	Description
Use case	Describes the relationships among the functionalities and their internal/external controllers. These controllers are known as actors.
Activity	Describes the flow of control in a system. It consists of activities and links. The flow can be sequential, concurrent, or branched.
State Machine/state chart	Represents the event driven state change of a system. It basically describes the state change of a class, interface, etc. Used to visualize the reaction of a system by internal/external factors.
Sequence	Visualizes the sequence of calls in a system to perform a specific functionality.
Interaction Overview	Combines activity and sequence diagrams to provide a control flow overview of system and business process.
Communication	Same as sequence diagram, except that it focuses on the object’s role. Each communication is associated with a sequence order, number plus the past messages.
Time Sequenced	Describes the changes by messages in state, condition and events.

Download 0.69 Mb.

Share with your friends: