Automated validation & verification of UML/OCL models using satisfiability solvers. ([2018])

• Record Type: Book
• Further Information: Note: Nils Przigoda, Robert Wille, Judith Przigoda, Rolf Drechsler.
• Authors: Przigoda, Nils; Wille, Robert; Przigoda, Judith; Drechsler, Rolf
• 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.
• Publisher Details: Cham : Springer
• Publication Date: 2018
• Copyright Date: 2018
• Extent: 1 online resource
• Subjects: 005.1/17; Engineering; Object-oriented methods (Computer science); UML (Computer science); Computer software -- Validation; Computer software -- Verification; COMPUTERS -- Programming -- Object Oriented; Computer software -- Validation; Computer software -- Verification; Object-oriented methods (Computer science); UML (Computer science); Engineering; Circuits and Systems; Processor Architectures; Electronics and Microelectronics, Instrumentation; Computers -- Systems Architecture -- General; Technology & Engineering -- Electronics -- General; Computer architecture & logic design; Electronics engineering; Systems engineering; Computer science; Electronics; Technology & Engineering -- Electronics -- Circuits -- General; Circuits & components; Electronic books
• Languages: English
• ISBNs: 9783319728148; 3319728148
• Related ISBNs: 9783319728131; 331972813X
• Notes: Note: Includes bibliographical references.; Note: Online resource; title from PDF title page (EBSCO, viewed January 30, 2018).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.