Linked e-resources
Details
Table of 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.
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.