Specification of Software Systems

Cover......Page 1
Specification of Software Systems, Second Edition......Page 3
ISBN 9780857292766......Page 4
Background and Motivation......Page 6
Part II......Page 7
How to Use the Book......Page 8
Intended Audience......Page 9
Acknowledgments......Page 10
General Characteristics......Page 12
Audience......Page 13
Organization and Content......Page 14
Case Studies......Page 15
How to Use the Book......Page 16
Acknowledgements......Page 17
Contents......Page 18
Part I
Specification Fundamentals......Page 28
1 The Role of Specification......Page 30
Software Complexity......Page 31
Structural Complexity......Page 33
Environmental Complexity......Page 34
Application Domain Complexity......Page 36
Communication Complexity......Page 37
Software Specification......Page 38
Why Specify?......Page 39
What to Specify?......Page 40
When to Specify?......Page 41
How to Control Complexity?......Page 42
Exercises......Page 45
Bibliographic Notes......Page 46
References......Page 48
2 Specification Activities......Page 50
Integrating Formal Methods into the Software Life-Cycle......Page 51
Level of Formality......Page 53
Tool......Page 54
Specification Roles......Page 55
Design Roles......Page 56
Implementation Roles......Page 57
Exercises......Page 58
References......Page 59
3 Specification Qualities......Page 62
Why a Programming Language Cannot Serve as a Specification Language?......Page 63
Abstraction......Page 65
Historical References......Page 66
Product Quality and Utility......Page 67
Precision......Page 68
Logical Reasoning......Page 69
Quality Dimensions and Quality Model......Page 70
Exercises......Page 71
References......Page 72
What Is Abstraction?......Page 74
Fundamental Abstractions in Computing......Page 75
Abstractions for Software Construction......Page 77
Domain Abstraction......Page 78
Environmental Abstraction......Page 80
System Abstractions......Page 81
Exercises......Page 82
References......Page 83
Part II
Formalism Fundamentals......Page 86
5 Formal Systems......Page 88
Peano\'s Axiomatization of Naturals-Formalization in Mathematics......Page 89
Formalization in Science......Page 90
Formalization Process in Software Engineering......Page 91
Syntax......Page 92
Semantics......Page 93
Inference Mechanism......Page 94
Properties of Formal Systems......Page 96
Completeness......Page 97
Extended Syntactic Metalanguage......Page 98
Exercises......Page 101
References......Page 103
6 Automata......Page 104
Deterministic Finite Accepters......Page 105
State Machine Modeling......Page 106
Language Recognizer......Page 107
Pattern Matching......Page 108
Finite Container......Page 110
Window Manager......Page 111
Nondeterministic Finite Accepters......Page 112
Composing nfas......Page 114
Choice......Page 115
Intersection......Page 116
Generalized Intersection......Page 118
Finite State Transducers......Page 120
Modeling Controllers with Discrete and Continuous Behaviors......Page 121
Exercises......Page 128
Bibliographic Notes......Page 129
References......Page 130
7 Extended Finite State Machine......Page 132
State Machine Hierarchy......Page 134
Menu-Driven User Interface Model......Page 137
Modularity and Bottom-up Construction......Page 140
Simulation......Page 145
Transition Points......Page 146
Case Study-Elevator Control......Page 147
Exercises......Page 151
References......Page 154
The Four Pillars......Page 156
Property-Oriented Specification Methods......Page 157
Model-Based Specification Techniques......Page 158
Languages Chosen for Discussion......Page 159
References......Page 160
Part III
Logic......Page 162
Syntax and Semantics......Page 164
Reasoning Based on Adopting a Premise......Page 166
Inference Based on Natural Deduction......Page 167
Proof by Resolution......Page 168
Consistency and Completeness......Page 170
Exercises......Page 171
References......Page 172
10 Predicate Logic......Page 174
Syntax and Semantics......Page 175
Semantics......Page 176
Equality and Equivalence......Page 178
More on Quantified Expressions......Page 181
Policy Language Specification......Page 182
Knowledge Representation......Page 185
Natural Deduction Process......Page 187
Clausal Forms......Page 189
Unification......Page 191
Decidability......Page 192
Hoare\'s Notation......Page 193
Conjunction and disjunction of specifications......Page 194
Program Exchange......Page 195
Program Division......Page 196
Exercises......Page 198
References......Page 201
11 Temporal Logic......Page 204
Temporal Logic for Specification and Verification......Page 205
Temporal Abstraction......Page 206
Discrete or Continuous......Page 207
Propositional Temporal Logic (PTL)......Page 208
Syntax......Page 209
Model and Semantics......Page 210
More Temporal Operators......Page 211
Axioms......Page 213
Formalizing Properties in PTL......Page 214
True Concurrency......Page 216
Executions Triggered by Messages......Page 217
Reactive System Specification: Rail Road Crossing Problem......Page 219
Behavior of Gate......Page 220
Behavior of Controller-Gate Interaction......Page 221
First Order Temporal Logic (FOTL)......Page 222
Formalizing Properties in FOTL......Page 223
Semantics of Conditional Statement......Page 226
Semantics of Repetition Statement......Page 227
Component Specification......Page 228
Specifications......Page 230
Verification of Simple FOTL Specifications......Page 232
Proving Invariant Property......Page 234
Hanoi Specification......Page 235
Model Checking......Page 237
Program Graphs, Transition Systems, and Kripke Structures......Page 239
Model Checking using Büchi Automata......Page 244
Model Checking Procedure......Page 245
Computing Product of Büchi Automata......Page 246
Exercises......Page 248
Bibliographic Notes......Page 253
References......Page 255
Part IV Mathematical Abstractions for Model-Based Specifications......Page 258
Formal Specification Based on Set Theory......Page 260
Set Notation......Page 261
Reasoning with Sets......Page 262
A Specification Example......Page 264
Relations and Functions......Page 269
Functions on Relations......Page 271
Proof by Cases......Page 275
Proof by Induction......Page 276
A Specification Example......Page 278
Sequence Operators......Page 281
Proofs......Page 284
A Specification Example......Page 288
Exercises......Page 289
Bibliographic Notes......Page 290
References......Page 291
Part V
Property-Oriented Specifications......Page 292
Algebra and Specification......Page 294
Algebras-A Brief Introduction......Page 297
Homogeneous Algebras......Page 298
Heterogeneous Algebras......Page 299
Abstract Data Types......Page 300
Presentation......Page 301
Semantics......Page 303
Reasoning......Page 304
Extending Many-Sorted Specifications......Page 306
Classification of Operations......Page 307
Adequacy......Page 308
Structured Specifications......Page 309
OBJ3-An Algebraic Specification Language......Page 313
OBJ3 Basic Syntax......Page 315
Built-in Sorts......Page 317
Order-Sorted Algebra......Page 318
Import Clause......Page 319
Associativity and Commutativity......Page 320
Signature and Equations......Page 321
Signature of a Module......Page 322
Parameterized Programming......Page 323
Theories......Page 324
Parameterized Modules......Page 325
Instantiation......Page 326
Module Expression......Page 328
Requirements......Page 329
Formal Specifications......Page 330
Exercises......Page 336
Bibliographic Notes......Page 337
References......Page 338
The Two Tiers of Larch......Page 340
Equational Specification......Page 342
More Expressive Specifications and Stronger Theories......Page 346
Renaming......Page 348
Stating Checkable Properties......Page 349
Completeness......Page 350
Stating Assumptions......Page 351
Operator Overloading......Page 353
In-line Traits......Page 354
More LSL Examples......Page 356
File......Page 357
Enriching List Trait......Page 358
Iterator......Page 359
Date and Zone......Page 360
Time......Page 363
Larch/C++: A Larch Interface Specification Language for C++......Page 366
Relating Larch/C++ to C++......Page 368
The Formal Model of Objects, Values and States......Page 369
Declarations and Declarators......Page 370
State Functions......Page 371
Larch/C++ Syntax-An Example......Page 372
Function Specification......Page 373
Proofs in LSL......Page 375
Proof Obligations......Page 376
LP theories......Page 378
Operator Theories......Page 379
Normalization......Page 380
Proof by Induction......Page 381
RWZone Specification......Page 382
RWFile Specification......Page 383
Exercises......Page 385
References......Page 390
15 Calculus of Communicating Systems......Page 392
Why a Specific Calculus for Concurrency Is Necessary?......Page 394
Action Prefix......Page 395
Definition......Page 396
Sum (Choice)......Page 397
Communication......Page 398
Restriction......Page 401
Conditional Constructor......Page 402
Relabeling......Page 403
Syntax......Page 404
The Operational Semantics of Agents......Page 405
Simulation and Equivalence......Page 410
Derivation Trees......Page 411
Milner\'s Laws......Page 414
Labeled Transition Systems-Some Properties......Page 418
Trace Equivalence......Page 419
Equivalence and Congruence......Page 421
Substitutability and Strong Bisimilarity......Page 423
Expansion Principle......Page 424
Law2-Recursion......Page 425
Exercises......Page 426
Bibliographic Notes......Page 428
References......Page 429
Part VI Model-Based Specifications......Page 430
Structure of a VDM Specification......Page 432
Representational Abstraction......Page 433
Simple Types......Page 434
Quote Types......Page 435
Union Type......Page 436
Sequence......Page 437
Map......Page 439
Record......Page 441
Function Types......Page 442
Patterns, Bindings and Values......Page 443
State Representation......Page 444
State Invariant......Page 447
Let Expression......Page 448
Implicit Function......Page 449
Explicit Function......Page 450
Operation Definitions......Page 451
Implicit Operation......Page 452
Explicit Operation......Page 453
Cases Statement......Page 454
Specification Examples......Page 457
Case Study-Computer Network......Page 467
Rigorous Reasoning......Page 474
Data Refinement......Page 476
Proof Obligations......Page 477
Example for Data Refinement......Page 478
Domain Obligation......Page 479
Operation Decomposition......Page 480
Example for Operation Decomposition......Page 481
Exercises......Page 482
Bibliographic Notes......Page 484
References......Page 485
Representational Abstraction......Page 488
Simple Types......Page 489
Tuples and Cartesian Product Types......Page 490
Abbreviation......Page 491
Relations and Functions......Page 492
Sequences......Page 493
Bags......Page 494
Operators on Bags......Page 495
Free Types......Page 497
Schemas......Page 498
Schema Types and Bindings......Page 499
Type Compatibility of Signatures......Page 500
Schema Inclusion......Page 501
Remarks......Page 502
Generic Schema......Page 503
Schema Expressions......Page 504
Schema Renaming......Page 506
Schema Hiding and Projection......Page 507
State Representation......Page 508
Operations......Page 509
Schema Decorators and Conventions......Page 511
Sequential Composition......Page 514
Functions......Page 515
Generic Functions......Page 516
Specification Examples......Page 517
Proving Properties from Z Specifications......Page 532
One-Point-Rule......Page 533
Consistency of Operations......Page 536
Case Study: An Automated Billing System......Page 540
Additional Features in Z......Page 548
Precondition Calculation......Page 549
Precondition Simplification......Page 550
Promotion......Page 551
Refinement and Proof Obligations......Page 553
Data Refinement......Page 554
Abstract Specification......Page 556
Concrete Specification......Page 557
Proof Obligations......Page 558
Exercises......Page 561
Bibliographic Notes......Page 563
References......Page 564
Basic Structure of an Object-Z Specification......Page 566
Parameterized Class......Page 569
Inheritance......Page 571
Polymorphism......Page 574
Sequential Composition Operator......Page 575
Concurrency Operator......Page 576
Parallel Communication Operator......Page 577
Environment Enrichment Operator......Page 578
Specification Examples......Page 579
Case Study......Page 591
Exercises......Page 598
Bibliographic Notes......Page 600
References......Page 601
Abstract Machine Notation (AMN)......Page 604
Structure of a B Specification......Page 605
Arrays......Page 609
ANY Statement......Page 611
CHOICE Statement......Page 612
PRE Statement......Page 613
The INCLUDES Clause......Page 614
The USES Clause......Page 618
The SEES Clause......Page 621
Sequential Composition of Statements......Page 623
Refinement Machine......Page 624
Specification Examples......Page 627
Case Study-A Ticketing System in a Parking Lot......Page 640
Proof Obligations......Page 650
Maintaining the State Invariant......Page 652
Proof Obligations for INCLUDES Clause......Page 653
Proof Obligations for USES Clause......Page 654
Proof Obligations for Refinement......Page 655
Exercises......Page 657
Bibliographic Notes......Page 658
References......Page 659
Index......Page 662