CORRECTNESS, SPECIFICATIONS AND UNITY – Project topics materials

Get Complete Project Material File(s) Now! »

INTRODUCTION

The characteristics of the SLOOP method can be divided into two broad categories, viz. software correctness and object-orientation. This chapter serves as an introduction to the issues related to the software correctness aspects of the method. Similarly, Chapter 3 covers object-oriented aspects. Together these two chapters provide the background to the concepts on which the SLOOP method is based.

The software correctness coundrum

One could ask why software correctness warrants so much research. The main reason is that software is complex and therefore difficult to get right. There are many properties that distinguish software engineering from other engineering disciplines. Parnas et al. [PvSK90] list a few differences: The nature of the errors. An error lies dormant in the system until the necessary sequence of events is executed to trigger it. Errors are not introduced due to wear. For example, in the case of hardware, errors due to wear-out cimbe detected by running diagnostic tests. Tolerance.
In most engineering disciplines it is good enough to get it almost right. This is based on the fact that the effect of an error is directly proportional to the size of the error. This is not true for software. A punctuation error can cause havoc, while it is possible that a major design oversight can be tolerated. Thus far no useful definition of tolerance exists for software. Inconclusive testing. A huge number of tests needs to be performed before one can be reasonably confident about the software. However, it still does not mean that there are no errors. This is a result of the fact that the mathematical functions describing the software may contain an arbitrary number of discontinuities. This property gives software its flexibility, but also its complexity.

Validation, a posteriori program verification and the « constructive

approach » The above problems are formidable when dealing with sequential programs; they become even more daunting when concurrency is introduced. Due to the multitude of ways in which the processes can interact with one another, there is a myriad of sequences of events that needs to be tested. System testing, i.e. executing a system in order to check that it meets user requirements, is an example of validation [Ince93]. Validation is concerned with checking that the product of a phase matches user requirements [Ince93].

Categories of correctness properties

In order to produce unambiguous specifications one has to define correctness properties in more rigorous terms. Partial and total correctness are useful properties of sequential programs that are supposed to terminate. A program that satisfies the partial correctness property guarantees that if the precondition that restricts the set of input values is satisfied, then the resulting output values will be correct if the program terminates. Note that it does not guarantee termination. Total correctness, on the other hand, guarantees termination as well. Formal definitions of these properties are presented in Sections 2.4.4.1 and 2.4.5.1 respectively.

1. INTRODUCTION
1.1 The problem
1.2 The goals
1.3 Towards a new method
1.3.1 The object-oriented paradigm
1.3.2 UNITY
1.3.3 Formal methods
1.3.4 Computational reflection
1.3.5 The resulting method: SLOOP
1.4 Related work
1.5 The contribution
1.6 Structure of the thesis
2. CORRECTNESS, SPECIFICATIONS AND UNITY
2.1 Introduction
2.2 The software correctness conundrum
2.2.1 Validation, a posteriori program verification and the « constructive approach »
2.2.2 Categories of correctness properties
2.3 Modelling concurrency
2.3.1 Interleaving
2.3.2 Atomicity and interference
2.3. 3 Fairness
2.4 Formulating correctness properties
2.4.1 Temporal logic
2.4.2 Temporal operators
2.4.3 Which correctness properties?
2.4.4 Safety properties
2.4.4.1 Partial correctness
2.4.4.2 Clean behaviour
2.4.4.3 Global and local invariants
2.4.4.4 Mutual exclusion
2.4.4.5 Deadlock freedom
2.4.4.6 Generalised deadlock freedom
2.4.5 Liveness properties
2.4.5.1 Total correctness
2.4.5.2 Intermittent assertions
2.4.5.3 Accessibility
2.4.5.4 Liveness
2.4.5.5 Responsiveness
2.4.6 Precedence properties
2.4.6.1 Safe liveness
2.4.6.2 Absence of unsolicited response
2.4.6.3 Fair responsiveness
2.5 UNITY
2.5.1 Non-determinism
2.5.2 Assignments and absence of controlflow
2.5.3 State transitions
2.5.4 Program structuring
2.5.5 A logic for the specification, design and verification of UNITY programs
3. THE OBJECT-ORIENTED PARADIGM
3.1 Introduction
3.2 Object-orientation and concurrency
3.2.1 Multiple threads of control
3.2.2 Synchronisation
3.2.2.1 The semantics of operation invocations
3.2.2.2 Race conditions
3.2.2.3 Synchronisation constraints
3.3 Design patterns and frameworks
3.3.1 Categories of patterns
3.3.2 Advantages of using design patterns
3.3.3 Design patterns and formalisation
3.3.4 Frameworks
3.4 Specifying object interaction
3.5 Object-oriented formal methods
3.6 Summary
4. THE SLOOP METHOD
4.1 Introduction
4.2 Overview of the SLOOP method
4.2.1 The SLOOP computational model
4.2.2 The main components of the method
4.2.3 The crux of the method
4.3 The structure of a SLOOP program
4.3.1 The SLOOP-program ,
4.3.2 SLOOP classes
4.3.3 The macros-section
4.3.3.1 Purpose of the macros-section
4.3.3.2 The syntax
4.3.3.3 Example usage
4.3.4 The properties-section
4.3 4.1 The syntax
4.3.4.2 Reuse of correctness properties
4.3.4.3 Class properties and method properties
4.3.4.4 Definitions of the logical relations
4.3.4.5 Method properties and the value returned by a method
4.3.5 The methods-section
4.3.5.1 The methods-section syntax
4.3.5.2 Method invocation
4.3.5.3 Parallel method activation and the number of active parallel statements
4.3.5.4 Nesting of SLOOP method invocations
4.3.5.5 SLOOP objects and events
4.3.6 The SLOOP statement-list
4.3.6.1 The syntax
4.3.6.2 Statements, components and parts
4.3.6.3 Evaluation order
4.3.6.4 The simplification of reasoning about correctness
4.3.6.5 Prevention of deadlock
4.3.7 The SLOOP method and inheritance, encapsulation and polymorphism
4.4 Seamless analysis, design and implementation
4.4.1 The requirements analysis phase
4.4.2 The design phase
4.4.3 The implementation phase
404.3.1 Mapping the activation-section
4.4.3.2 Mapping a package
404.3.3 Mapping a class and its methods
4.5 Summary
5. REQUIREMENTS ANALYSIS FROM THE SLOOP PERSPECTIVE
5.1 Introduction
5.2 Useful correctness properties
5.2.1 Safety properties
5.2.1.1 Partial correctness
5.2.1.2 Clean behaviour
5.2.1.3 Global and local invariants
5.2.1.4 Mutual exclusion
5.2.1.5 Deadlock freedom
5.2.1.6 Generalised deadlock freedom
5.2.1.7 Unless property
5.2.2 Liveness properties
5.2.2.1 Total correctness
5.2.2.2 Intermittent assertions
5.2.2.3 Accessibility
5.2.204 Liveness (absence of individual starvation)
5.2.2.5 Responsiveness
5.2.3 Precedence properties
5.2.3.1 Safe liveness
5.2.3.2 Absence of unsolicited response
5.2.3.3 Fair responsiveness
5.2.4 SLOOP checklist of correctness properties
5.3 Constructing the class diagram
5.3.1 Initial informal problem statement
5.3.2 The class diagram
5.4 Specifying system behaviour informally
5.4.1 Safety properties
504.1.1 AS 1-yy (partial correctness)
504.1.2 AS2-yy (clean behaviour)
504.1.3 AS3-yy (global invariants)
504.104 AS4-yy (unless properties)
5.4.2 Liveness properties
504.2.1 ALl-yy (total correctness)
504.2.2 AL2-yy (intermittent assertions)
504.2.3 AL3-yy (responsiveness)
5.4.3 Precedence properties
504.3.1 AP 1-yy (safe liveness)
504.3.2 AP2-yy (absence of unsolicited response)
5.4.3.3 AP3-yy (fair responsiveness)
5.4.4 Consolidation
5.4.5 Informal specification of correctness properties of individual classes
504.5.1 The CommsProviderSimulator class
504.5.2 The ServiceProviderSimulator class
5.4.6 Summary of the requirements analysis phase steps
5.5 Summary
6. DESIGN FROM THE SLOOP PERSPECTIVE
6.1 Introduction
6.2 Identifying reusable artifacts
6.2.1 Mappingproblem domain objects onto solution domain objects
6.2.2 Formal versus informal specification of class properties
6.2.3 Reusing existing classes through inheritance
6.2.4 Discovering suitable existing classes after design level refinements
6.3 Refining the specification
6.3.1 The role of correctness properties during design level refinements
6.3.2 The impact of the computational model on design level decisions
6.4 Formalising correctness properties
6.5 Deriving SLOOP statements
6.6 Constructing the SLOOP program
6.6.1 Using the results of the design phase refinements to determine the contents
of the sequential methods of the activation classes
6.6.2 Determining the contents of the parallel methods of the activation classes
6.7 Making the design more reusable
6.8 Summary
7. REASONING ABOUT SLOOP PROGRAMS
7.1 Introduction
7.1.1 Conveying the semantics
7.1.2 Reasoning about correctness
7.1.3 Reusability
7.1.4 Absence of control flow
7.1.5 Using correctness properties to derive SLOOP statements
7.2 Conveying the semantics
7.2.1 The static nature of a class
7.2.2 The dynamic nature of a class
7.3 The impact of various SLOOP features on correctness reasoning
7.3.1 Safety properties.
7.3.1.1 Using the correctness arguments of a clean behaviour property to illustrate how the use of macros in SLOOP programs can simplify correctness reasoning.
7.3.1.2 Demonstrating how the computational model and object-oriented features such as data encapsulation and reusability influence the approach followed during correctness reasoning
7.3.1.3 Using a global invariant property to discuss the responsibility of the client object regarding preconditions in correctness properties
7.3.1.4 Using an unless property to demonstrate how the correctness properties
specified for the class itself as well as those inherited from its parent class are applied in correctness arguments
7.3.2 Liveness properties
7.3.2.1 Showing why the postconditions of a total correctness property can be used in an ensures relation
7.3.2.2 Using an intermittent assertion property to demonstrate how the repeated execution of parallel statements guarantees progress, provided the preconditions hold at some point
7.3.2.3 Using a responsiveness property to demonstrate the importance of showing that the preconditions will eventually hold when reusing other correctness properties in the correctness arguments of a liveness property
7.3.3 Precedence properties
7.3.3.1 Using a safe liveness property to highlight the impact of the postconditions: and postconditions:withArguments: constructs on correctness arguments
7.3.3.2 Using an absence of unsolicited reponse property to demonstrate how the characteristics of an ensures relation can be used in correctness arguments
7.3.3.3 Using a fair responsiveness property to illustrate the importance of showing via correctness arguments that the selection of the constituent classes of a system will indeed result in the behaviour as described in the specification of the system
7.4 Deriving SLOOP statements from correctness properties
7.5 Summary
8. THE IMPLEMENTATION PHASE
8.1 Introduction
8.2 Mappings to various architectures
8.2.1 Sequential architectures
8.2.2 Synchronous shared-memory architectures
8.2.3 Asynchronous shared-memory architectures
8.2.4 Distributed systems
8.2.5 Comparison with UNITY mappings
8.3 Deriving executable programs on various architectures
8.3.1 Sequential architectures
8.3.2 Synchronous shared-memory architectures
8.3.3 Asynchronous shared-memory architectures
8.3.4 Distributed systems
8.3.4.1 Guaranteeing absence of deadlock in a mapping to a distributed architecture
8.3.4.2 Identifying the objects that need to be reserved
8.3.4.3 The middleware infrastructure
8.4 Mapping macros
8.5 Mapping SLOOP statements ;
8.5.1 Mapping quantified-statement-lists
8.5.1 Mapping statement-components and component-parts
8.6 The use of reflection in mappings of SLOOP programs
8.6.1 A reflective computation infrastructure
8.6.2 Using reflective computation for control purposes
8.6.3 Using reflective computation for assertion checking
8.7 Modifying the level of parallelism in a SLOOP design
8.8 Summary
9. INCORPORATING DESIGN PATTERNS INTO A SLOOP DESIGN
9.1 Introduction
9.2 Architectural patterns
9.2.1 Pipes and filters
9.2.2 Reflection
9.3 Creational design patterns
9.3.1 The Factory Method
9.3.2 Singleton
9.4 Structural design patterns
9.4.1 Adapter.
9.4.2 Flyweight
9.4.3 Proxy
9.5 Behavioural design patterns
9.5.1 Iterator
9.5.2 State
9.5.3 Template
9.5.4 Strategy
9.6 Summary
10. CONCLUSION
10.1 Evaluation of the SLOOP method
10.1.1 Increasing the reliability of systems developed via this method
10.1.2 Scalability of the method
10.1.3 Understandability of the method
10.1.4 Unified approach
10.1.5 Reusability
10.1.6 Seamlessness
10.1.7 General availability and minimisation of developmental resources
10.2 Concluding remarks and future research directions