000825815 000__ 05708cam\a2200577Ii\4500
000825815 001__ 825815
000825815 005__ 20230306144235.0
000825815 006__ m\\\\\o\\d\\\\\\\\
000825815 007__ cr\cn\nnnunnun
000825815 008__ 180125t20182018sz\\\\\\ob\\\\000\0\eng\d
000825815 019__ $$a1021192210$$a1027054866
000825815 020__ $$a9783319728148$$q(electronic book)
000825815 020__ $$a3319728148$$q(electronic book)
000825815 020__ $$z9783319728131
000825815 0247_ $$a10.1007/978-3-319-72814-8$$2doi
000825815 035__ $$aSP(OCoLC)on1020319109
000825815 035__ $$aSP(OCoLC)1020319109$$z(OCoLC)1021192210$$z(OCoLC)1027054866
000825815 040__ $$aN$T$$beng$$erda$$epn$$cN$T$$dN$T$$dGW5XE$$dEBLCP$$dAZU$$dUAB$$dUPM$$dMERER$$dOCLCF$$dOCLCQ
000825815 049__ $$aISEA
000825815 050_4 $$aQA76.9.O35
000825815 08204 $$a005.1/17$$223
000825815 1001_ $$aPrzigoda, Nils,$$eauthor.
000825815 24510 $$aAutomated validation & verification of UML/OCL models using satisfiability solvers /$$cNils Przigoda, Robert Wille, Judith Przigoda, Rolf Drechsler.
000825815 264_1 $$aCham :$$bSpringer,$$c[2018]
000825815 264_4 $$c©2018
000825815 300__ $$a1 online resource
000825815 336__ $$atext$$btxt$$2rdacontent
000825815 337__ $$acomputer$$bc$$2rdamedia
000825815 338__ $$aonline resource$$bcr$$2rdacarrier
000825815 347__ $$atext file$$bPDF$$2rda
000825815 504__ $$aIncludes bibliographical references.
000825815 5050_ $$aIntro; 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.
000825815 5058_ $$a3.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.
000825815 5058_ $$a4.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.
000825815 5058_ $$a5.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.
000825815 5058_ $$a5.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.
000825815 506__ $$aAccess limited to authorized users.
000825815 520__ $$aThis 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.
000825815 588__ $$aOnline resource; title from PDF title page (viewed January 30, 2018).
000825815 650_0 $$aObject-oriented methods (Computer science)
000825815 650_0 $$aUML (Computer science)
000825815 650_0 $$aComputer software$$xValidation.
000825815 650_0 $$aComputer software$$xVerification.
000825815 7001_ $$aWille, Robert,$$eauthor.
000825815 7001_ $$aPrzigoda, Judith,$$eauthor.
000825815 7001_ $$aDrechsler, Rolf,$$eauthor.
000825815 77608 $$iPrint version: $$z9783319728131
000825815 852__ $$bebk
000825815 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-319-72814-8$$zOnline Access$$91397441.1
000825815 909CO $$ooai:library.usi.edu:825815$$pGLOBAL_SET
000825815 980__ $$aEBOOK
000825815 980__ $$aBIB
000825815 982__ $$aEbook
000825815 983__ $$aOnline
000825815 994__ $$a92$$bISE