| Description |
1 online resource |
| Contents |
Intro; Preface; Contents; Nomenclature; 1 Introduction; 2 A Formal Interpretation of UML/OCL; 2.1 Type System; 2.2 Classes and Models; 2.3 Objects and System States; 2.4 Invariants, Pre-, and Postconditions; 2.5 Decision Problems; 2.5.1 Boolean Satisfiability; 2.5.2 Satisfiability Modulo Theories; 3 A Symbolic Formulation for Models; 3.1 A General Flow for Automatic Verification and Validation; 3.2 Transforming a Model into a Symbolic Formulation; 3.2.1 Transforming Attributes; 3.2.2 Transforming Associations; 3.2.3 Handling a Fixed and Variable Number of Objects |
|
3.2.4 Handling Null and Invalid3.2.5 Transforming OCL Constraints; 3.3 Adding Verification Tasks; 3.3.1 Structural Verification Tasks; 3.3.2 Behavioral Verification Tasks; 3.4 Other Approaches for Model Validation and Verification; 4 Structural Aspects; 4.1 Debugging Inconsistent Models; 4.1.1 Problem Formulation; 4.1.2 Previously Proposed Solutions; 4.1.3 Proposed Approach; 4.1.4 Implementation and Evaluation; 4.1.4.1 Straightforward Approach; 4.1.4.2 Optimized Approach; 4.1.5 Comparison with Other Approaches, Also from Different Fields; 4.1.6 Example of Use |
|
4.2 Analyzing Invariant Independence4.2.1 Independence in Formal Models; 4.2.2 Analysis for Invariant Independence; 4.2.3 Proposed Solution; 4.2.3.1 Advanced Problem Formulation; 4.2.3.2 Determining Minimal Reasons for Dependent Invariants; 4.2.4 Experimental Evaluation; 4.2.4.1 Evaluation of the Runtime Performance; 4.2.4.2 Quality of the Results; 4.3 Relation to Similar Approaches Used in SAT/SMT Solving; 5 Behavioral Aspects; 5.1 Restricting State Transitions Using Frame Conditions; 5.1.1 Related Work; 5.1.2 Integrating Frame Conditions in the Symbolic Formulation |
|
5.1.2.1 Changes to the UML/OCL Model Definitions5.1.2.2 Adding Constraints for Frame Conditions; 5.1.2.3 Dealing with Object Creation and Deletion; 5.1.2.4 Implementation; 5.1.3 Deriving Frame Conditions from the AST; 5.1.3.1 Remaining Problems with Frame Conditions; 5.1.3.2 Interpretation Semantics; 5.1.3.3 General Idea; 5.1.3.4 Remarks; 5.2 Moving on to Concurrent Behavior in the Symbolic Formulation; 5.2.1 Problem Formulation and Related Work; 5.2.1.1 Related Work and Considered Problem; 5.2.1.2 Considered Computational Model; 5.2.1.3 Supporting Concurrent Behavior |
|
5.2.2 Handling Contradictory Conditions5.2.3 Implementation and Application; 5.2.3.1 Considered Model; 5.2.3.2 Application; 6 Timing Aspects; 6.1 Preliminaries About Clocks and Ticks; 6.2 A Generic Representation of CCSL Constraints; 6.2.1 Determining the Generic Representation; 6.2.1.1 Initializing the Automaton; 6.2.1.2 Applying Constraints; 6.2.2 Discussion and Application of the Generic Representation; 6.2.2.1 Application and Comparison to Related Work; 6.2.2.2 Exemplary Evaluation; 6.3 Validation of Clock Constraints Against Instant Relations; 6.3.1 Motivation and Proposed Idea |
| Summary |
This book provides a comprehensive discussion of UML/OCL methods and design flow, for automatic validation and verification of hardware and software systems. While the presented flow focuses on using satisfiability solvers, the authors also describe how these methods can be used for any other automatic reasoning engine. Additionally, the design flow described is applied to a broad variety of validation and verification tasks. The authors also cover briefly how non-functional properties such as timing constraints can be handled with the described flow. Provides a general flow and description for the validation and verification of UML/OCL models; Demonstrates a detailed realization of the general flow using satisfiability solvers; Includes a case study that presents the possibilities of the state-of-the-art approaches |
| Bibliography |
Includes bibliographical references |
| Notes |
Online resource; title from PDF title page (EBSCO, viewed January 30, 2018) |
| Subject |
Object-oriented methods (Computer science)
|
|
UML (Computer science)
|
|
Computer software -- Validation.
|
|
Computer software -- Verification.
|
|
Computer programs -- Validation.
|
|
Computer programs -- Verification.
|
|
Computer architecture & logic design.
|
|
Electronics engineering.
|
|
Circuits & components.
|
|
COMPUTERS -- Programming -- Object Oriented.
|
|
Computer software -- Validation
|
|
Computer software -- Verification
|
|
Object-oriented methods (Computer science)
|
|
UML (Computer science)
|
| Form |
Electronic book
|
| Author |
Wille, Robert, author
|
|
Przigoda, Judith, author
|
|
Drechsler, Rolf, author
|
| ISBN |
9783319728148 |
|
3319728148 |
|
