Formal Engineering For Industrial Software Development

by Liu, Shaoying

• ISBN13: 9783540206026
• ISBN10: 3540206027
• eBook ISBN(s): 9783662072875
• Format: Hardcover
• Copyright: 2004-05-30
• Publisher: Springer-Verlag New York Inc
• More Book Details
• Purchase Benefits

Summary

In any serious engineering discipline, it would be unthinkable to construct a large system without having a precise notion of what is to be built and without verifying how the system is expected to function. Software engineering is no different in this respect. Formal methods involve the use of mathematical notation and calculus in software development; such methods are difficult to apply to large-scale systems with practical constraints (e.g., limited developer skills, time and budget restrictions, changing requirements). Here Liu claims that formal engineering methods may bridge this gap. He advocates the incorporation of mathematical notation into the software engineering process, thus substantially improving the rigor, comprehensibility and effectiveness of the methods commonly used in industry. This book provides an introduction to the SOFL (Structured Object-Oriented Formal Language) method that was designed and industry-tested by the author. Written in a style suitable for lecture courses or for use by professionals, there are numerous exercises and a significant real-world case study, so the readers are provided with all the knowledge and examples needed to successfully apply the method in their own projects.

Author Biography

 Shaoying Liu holds a B.Sc and a M.Sc degree in Computer Science from Xi'an Jiaotong University, China, and a Ph.D in Formal Methods from the University of Manchester, U.K. He worked as an Assistant Lecturer and then Lecturer at Xi'an Jiaotong University, a Research Associate at the University of York, and a Research Assistant at the Royal Holloway and Bedford New College of the University of London, respectively, in the period of 1982 -- 1994. He joined the Department of Computer Science at Hiroshima City University as an Associate Professor in April 1994, and then became a faculty member of the Department of Computer Science of the Faculty of Computer and Information Sciences at Hosei University in April 2000. In April 2001 he was promoted to a full Professor . He was invited as a Visiting Research Fellow by The Queen's University of Belfast from December 1994 to February 1995, and a Visiting Professor to Oxford University from December 1998 to February 1999. He is a member of IEEE Computer Society.

Table of Contents

1 Introduction	1	(20)
1.1 Software Life Cycle	2	(2)
1.2 The Problem	4	(1)
1.3 Formal Methods	5	(5)
1.3.1 What Are Formal Methods	5	(2)
1.3.2 Some Commonly Used Formal Methods	7	(2)
1.3.3 Challenges to Formal Methods	9	(1)
1.4 Formal Engineering Methods	10	(3)
1.5 What Is SOFL	13	(3)
1.6 A Little History of SOFL	16	(1)
1.7 Comparison with Related Work	17	(2)
1.8 Exercises	19	(2)
2 Propositional Logic	21	(16)
2.1 Propositions	21	(1)
2.2 Operators	22	(1)
2.3 Conjunction	23	(1)
2.4 Disjunction	24	(1)
2.5 Negation	24	(1)
2.6 Implication	25	(1)
2.7 Equivalence	25	(1)
2.8 Tautology, Contradiction, and Contingency	26	(1)
2.9 Normal Forms	27	(1)
2.10 Sequent	27	(1)
2.11 Proof	28	(6)
2.11.1 Inference Rules	28	(1)
2.11.2 Rules for Conjunction	29	(1)
2.11.3 Rules for Disjunction	29	(1)
2.11.4 Rules for Negation	30	(1)
2.11.5 Rules for Implication	30	(1)
2.11.6 Rules for Equivalence	30	(1)
2.11.7 Properties of Propositional Expressions	31	(3)
2.12 Exercises	34	(3)
3 Predicate Logic	37	(16)
3.1 Predicates	37	(3)
3.2 Quantifiers	40	(4)
3.2.1 The Universal Quantifier	40	(1)
3.2.2 The Existential Quantifier	41	(1)
3.2.3 Quantified Expressions with Multiple Bound Variables	42	(1)
3.2.4 Multiple Quantifiers	43	(1)
3.2.5 de Morgan's Laws	43	(1)
3.3 Substitution	44	(2)
3.4 Proof in Predicate Logic	46	(1)
3.4.1 Introduction and Elimination of Existential Quantifiers	46	(1)
3.4.2 Introduction and Elimination of Universal Quantifiers	46	(1)
3.5 Validity and Satisfaction	47	(1)
3.6 Treatment of Partial Predicates	48	(2)
3.7 Formal Specification with Predicates	50	(1)
3.8 Exercises	50	(3)
4 The Module	53	(64)
4.1 Module for Abstraction	53	(2)
4.2 Condition Data Flow Diagrams	55	(1)
4.3 Processes	56	(12)
4.4 Data Flows	68	(3)
4.5 Data Stores	71	(8)
4.6 Convention for Names	79	(1)
4.7 Conditional Structures	79	(2)
4.8 Merging and Separating Structures	81	(3)
4.9 Diverging Structures	84	(2)
4.10 Renarning Structure	86	(1)
4.11 Connecting Structures	87	(1)
4.12 Important Issues on CDFDs	88	(9)
4.12.1 Starting Processes	89	(1)
4.12.2 Starting Nodes	90	(1)
4.12.3 Terminating Processes	90	(1)
4.12.4 Terminating Nodes	91	(1)
4.12.5 Enabling and Executing a CDFD	91	(1)
4.12.6 Restriction on Parallel Processes	92	(2)
4.12.7 Disconnected CDFDs	94	(2)
4.12.8 External Processes	96	(1)
4.13 Associating CDFD with a Module	97	(7)
4.14 How to Write Comments	104	(1)
4.15 A Module for the ATM	104	(3)
4.16 Compound Expressions	107	(4)
4.16.1 The if-then-else Expression	107	(1)
4.16.2 The let Expression	108	(1)
4.16.3 The case Expression	109	(1)
4.16.4 Reference to Pre and Postconditions	110	(1)
4.17 Function Definitions	111	(3)
4.17.1 Explicit and Implicit Specifications	111	(2)
4.17.2 Recursive Functions	113	(1)
4.18 Exercises	114	(3)
5 Hierarchical CDFDs and Modules	117	(16)
5.1 Process Decomposition	117	(6)
5.2 Handling Stores in Decomposition	123	(1)
5.3 Input and Output Data Flows	124	(3)
5.4 The Correctness of Decomposition	127	(2)
5.5 Scope	129	(3)
5.6 Exercises	132	(1)
6 Explicit Specifications	133	(10)
6.1 The Structure of an Explicit Specification	133	(1)
6.2 Assignment Statement	134	(1)
6.3 Sequential Statements	135	(1)
6.4 Conditional Statements	135	(1)
6.5 Multiple Choice Statements	136	(1)
6.6 The Block Statement	137	(1)
6.7 The While Statement	137	(1)
6.8 Method Invocation	138	(1)
6.9 Input and Output Statements	139	(1)
6.10 Example	139	(2)
6.11 Exercises	141	(2)
7 Basic Data Types	143	(8)
7.1 The Numeric Types	143	(2)
7.2 The Character Type	145	(1)
7.3 The Enumeration Types	146	(1)
7.4 The Boolean Type	147	(1)
7.5 An Example	148	(1)
7.6 Exercises	148	(3)
8 The Set Types	151	(14)
8.1 What Is a Set	151	(1)
8.2 Set Type Declaration	152	(1)
8.3 Constructors and Operators on Sets	153	(7)
8.3.1 Constructors	153	(1)
8.3.2 Operators	154	(6)
8.4 Specification with Set Types	160	(2)
8.5 Exercises	162	(3)
9 The Sequence and String Types	165	(14)
9.1 What Is a Sequence	165	(1)
9.2 Sequence Type Declarations	166	(1)
9.3 Constructors and Operators on Sequences	167	(7)
9.3.1 Constructors	167	(2)
9.3.2 Operators	169	(5)
9.4 Specifications Using Sequences	174	(2)
9.4.1 Input and Output Module	174	(1)
9.4.2 Membership Management System	175	(1)
9.5 Exercises	176	(3)
10 The Composite and Product Types	179	(212)
10.1 Composite Types	179	(5)
10.1.1 Constructing a Composite Type	179	(2)
10.1.2 Fields Inheritance	181	(1)
10.1.3 Constructor	182	(1)
10.1.4 Operators	182	(2)
10.1.5 Comparison	184	(1)
10.2 Product Types	184	(2)
10.3 An Example of Specification	186	(2)
10.4 Exercises	188	(3)
11 The Map Types	191	(1)
11.1 What Is a Map	191	(1)
11.2 The Type Constructor	192	(1)
11.3 Operators	193	(6)
11.3.1 Constructors	193	(1)
11.3.2 Operators	194	(5)
11.4 Specification Using a Map	199	(2)
11.5 Exercises	201	(2)
12 The Union Types	203	(1)
12.1 Union Type Declaration	203	(1)
12.2 A Special Union Type	204	(1)
12.3 Is Function	205	(1)
12.4 A Specification with a Union Type	205	(1)
12.5 Exercises	206	(3)
13 Classes	209	(1)
13.1 Classes and Objects	209	(5)
13.1.1 Class Definition	210	(3)
13.1.2 Objects	213	(1)
13.1.3 Identity of Objects	214	(1)
13.2 Reference and Access Control	214	(2)
13.3 The Reference of a Current Object	216	(1)
13.4 Inheritance	217	(5)
13.4.1 What Is Inheritance	217	(1)
13.4.2 Superclasses and Subclasses	218	(2)
13.4.3 Constructor	220	(1)
13.4.4 Method Overloading	220	(1)
13.4.5 Method Overriding	221	(1)
13.4.6 Garbage Collection	222	(1)
13.5 Polymorphism	222	(2)
13.6 Generic Classes	224	(2)
13.7 An Example of Class Hierarchy	226	(3)
13.8 Example of Using Objects in Modules	229	(3)
13.9 Exercises	232	(3)
14 The Software Development Process	235	(1)
14.1 Software Process Using SOFL	235	(1)
14.2 Requirements Analysis	236	(7)
14.2.1 The Informal Specification	237	(2)
14.2.2 The Semi-formal Specification	239	(4)
14.3 Abstract Design	243	(9)
14.4 Evolution	252	(1)
14.5 Detailed Design	252	(5)
14.5.1 Transformation from Implicit to Explicit Specifications	253	(2)
14.5.2 Transformation from Structured to Object-Oriented Specifications	255	(2)
14.6 Program	257	(1)
14.7 Validation and Verification	258	(1)
14.8 Adapting the Process to Specific Applications	259	(1)
14.9 Exercises	260	(1)
15 Approaches to Constructing Specifications	261	(1)
15.1 The Top-Down Approach	261	(4)
15.1.1 The CDFD-Module-First Strategy	262	(1)
15.1.2 The CDFD-Hierarchy-First Strategy	263	(1)
15.1.3 The Modules and Classes	264	(1)
15.2 The Middle-out Approach	265	(2)
15.3 Comparison of the Approaches	267	(1)
15.4 Exercises	268	(1)
16 A Case Study - Modeling an ATM	269	(1)
16.1 Informal User Requirements Specification	270	(3)
16.2 Semi-formal Functional Specification	273	(6)
16.3 Formal Abstract Design Specification	279	(8)
16.4 Formal Detailed Design Specification	287	(13)
16.5 Summary	300	(1)
16.6 Exercises	301	(2)
17 Rigorous Review	303	(1)
17.1 The Principle of Rigorous Review	303	(2)
17.2 Properties	305	(5)
17.2.1 Internal Consistency of a Process	305	(2)
17.2.2 Invariant-Conformance Consistency	307	(1)
17.2.3 Satisfiability	308	(1)
17.2.4 Internal Consistency of CDFD	309	(1)
17.3 Review Task Tree	310	(4)
17.3.1 Review Task Tree Notation	310	(2)
17.3.2 Minimal Cut Sets	312	(1)
17.3.3 Review Evaluation	313	(1)
17.4 Property Review	314	(5)
17.4.1 Review of Consistency Between Process and Invariant	314	(2)
17.4.2 Process Consistency Review	316	(1)
17.4.3 Review of Process Satisfiability	317	(1)
17.4.4 Review of Internal Consistency of CDFD	317	(2)
17.5 Constructive and Critical Review	319	(1)
17.6 Important Points	320	(1)
17.7 Exercises	321	(2)
18 Specification Testing	323	(1)
18.1 The Process of Testing	323	(2)
18.2 Unit Testing	325	(10)
18.2.1 Process Testing	326	(6)
18.2.2 Invariant Testing	332	(3)
18.3 Criteria for Test Case Generation	335	(3)
18.4 Integration Testing	338	(8)
18.4.1 Testing Sequential Constructs	339	(2)
18.4.2 Testing Conditional Constructs	341	(2)
18.4.3 Testing Decompositions	343	(3)
18.5 Exercises	346	(3)
19 Transformation from Designs to Programs	349	(1)
19.1 Transformation of Data Types	350	(1)
19.2 Transformation of Modules and Classes	351	(6)
19.3 Transformation of Processes	357	(5)
19.3.1 Transformation of Single-Port Processes	357	(3)
19.3.2 Transformation of Multiple-Port Processes	360	(2)
19.4 Transformation of CDFD	362	(7)
19.5 Exercises	369	(2)
20 Intelligent Software Engineering Environment	371	(1)
20.1 Software Engineering Environment	371	(2)
20.2 Intelligent Software Engineering Environment	373	(2)
20.3 Ways to Build an ISEE	375	(1)
20.3.1 Domain-Driven Approach	375	(1)
20.3.2 Method-Driven Approach	375	(1)
20.3.3 Combination of Both	376	(1)
20.4 ISEE and Formalization	376	(1)
20.5 ISEE for SOFL	377	(4)
20.5.1 Support for Requirements Analysis	377	(1)
20.5.2 Support for Abstract Design	378	(1)
20.5.3 Support for Refinement	378	(1)
20.5.4 Support for Verification and Validation	379	(1)
20.5.5 Support for Transformation	379	(1)
20.5.6 Support for Program Testing	379	(1)
20.5.7 Support for System Modification	380	(1)
20.5.8 Support for Process Management	380	(1)
20.6 Exercises	381	(2)
References	383	(8)
A Syntax of SOFL	391	(12)
A.1 Specifications	391	(1)
A.2 Modules	392	(1)
A.3 Processes	392	(2)
A.4 Functions	394	(1)
A.5 Classes	394	(1)
A.6 Types	395	(1)
A.7 Expressions	396	(1)
A.8 Ordinary Expressions	396	(5)
A.8.1 Compound Expressions	396	(1)
A.8.2 Unary Expressions	397	(1)
A.8.3 Binary Expressions	397	(1)
A.8.4 Apply Expressions	397	(2)
A.8.5 Basic Expressions	399	(1)
A.8.6 Constants	399	(1)
A.8.7 Simple Variables	400	(1)
A.8.8 Special Keywords	400	(1)
A.8.9 Set Expressions	400	(1)
A.8.10 Sequence Expressions	400	(1)
A.8.11 Map Expressions	401	(1)
A.8.12 Composite Expressions	401	(1)
A.8.13 Product Expressions	401	(1)
A.9 Predicate Expressions	401	(2)
A.9.1 Boolean Variables	401	(1)
A.9.2 Relational Expressions	401	(1)
A.9.3 Conjunction	402	(1)
A.9.4 Disjunction	402	(1)
A.9.5 Implication	402	(1)
A.9.6 Equivalence	402	(1)
A.9.7 Negation	402	(1)
A.9.8 Quantified Expressions	402	(1)
A.10 Identifiers	403	(1)
A.11 Character	403	(1)
A.12 Comments	403	(2)
Index	405