000727549 000__ 05236cam\a2200505Ii\4500 000727549 001__ 727549 000727549 005__ 20230306140926.0 000727549 006__ m\\\\\o\\d\\\\\\\\ 000727549 007__ cr\cn\nnnunnun 000727549 008__ 150609s2015\\\\gw\a\\\\ob\\\\101\0\eng\d 000727549 019__ $$a914151113 000727549 020__ $$a9783658099947$$qelectronic book 000727549 020__ $$a3658099941$$qelectronic book 000727549 020__ $$z9783658099930 000727549 035__ $$aSP(OCoLC)ocn910878048 000727549 035__ $$aSP(OCoLC)910878048$$z(OCoLC)914151113 000727549 040__ $$aN$T$$beng$$erda$$epn$$cN$T$$dGW5XE$$dN$T$$dOCLCO$$dIDEBK$$dEBLCP$$dYDXCP$$dOCLCO$$dDEBSZ$$dVLB 000727549 049__ $$aISEA 000727549 050_4 $$aQA76.9.F67$$bI58 2015eb 000727549 08204 $$a004.01/51$$223 000727549 1112_ $$aInternational Summer School on Methods and Tools for the Design of Digital Systems$$n(1st :$$d2015 :$$cBremen, Germany) 000727549 24510 $$aFormal modeling and verification of cyber-physical systems$$h[electronic resource] :$$b1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015 /$$cRolf Drechsler, Ulrich Kühne (eds.). 000727549 264_1 $$aWiesbaden :$$bSpringer Vieweg,$$c2015. 000727549 300__ $$a1 online resource (x, 313 pages) :$$billustrations. 000727549 336__ $$atext$$btxt$$2rdacontent 000727549 337__ $$acomputer$$bc$$2rdamedia 000727549 338__ $$aonline resource$$bcr$$2rdacarrier 000727549 504__ $$aIncludes bibliographical references and author index. 000727549 5050_ $$aPreface; Organization; Table of Contents; Verification of Embedded Real-time Systems; 1 Introduction; 2 Related Work; 2.1 Formal Verification of SystemC Designs; 2.2 Conformance Testing for Real-time Systems; 2.3 Automatic Test Generation for SystemC; 3 Preliminaries; 3.1 SystemC; 3.2 Uppaal Timed Automata; 4 VeriSTA; 5 Formal Semantics for SystemC; 6 Model Checking and Conformance Testing; 7 Evolutionary Generation of Timed Test Traces; 8 Experimental Results; 8.1 Results from the AMBA advanced high-performance bus; 8.2 Results from the ASR/ABS system; 9 Conclusion; Acknowledgements 000727549 5058_ $$a2.2 Definition and Semantics3 Numerical Simulation; 3.1 Solving ODEs; 3.2 Computing Trajectories and Jumps; 3.3 Accounting for Nondeterminism; 3.4 Verification by simulation; 4 Reachability Analysis; 4.1 Reachability Algorithm; 4.2 Piecewise Constant Dynamics; 4.3 Piecewise Affine Dynamics; 4.4 Nonlinear Dynamics; 5 Conclusions; References; Model Checking and Model-based Testing in the Railway Domain; 1 Introduction; 2 Formal Verification; 2.1 Verification by Bounded Model Checking and k-Induction; 2.2 Formal Modelling; 2.3 Method Summary; 3 Interlocking System Verification -- a Case Study 000727549 5058_ $$a3.1 The Novel Danish Interlocking Systems3.2 The Domain-specific Language for Interlocking Systems; 3.3 Framework Implementation; 3.4 Generated Models; 3.5 Generated Safety Conditions; 3.6 Invariant Strengthening; 3.7 Verification Experiments; 4 Model-based Testing; 4.1 Model-based Testing Terminology; 4.2 Overall Test Objectives for the Railway Application; 4.3 Semantic Domain: I/O State Transition Systems; 4.4 Complete Testing Strategies; 4.5 Test Requirements Enforced by Standards; 4.6 Generic Domain-specific Test Strategy; 4.7 Functional Decomposition and Equivalence Classes 000727549 5058_ $$a4.8 Further Test Reduction Heuristics5 Conclusion; Acknowledgments; References; Modeling Unknown Values in Test and Verification; 1 Introduction; 1.1 Unknown Values in Circuit Test; 1.2 Unknown Values in Verification; 1.3 Minimization/Maximization in Test and Verification; 2 Basics; 2.1 Boolean Satisfiability and Extensions; 2.2 Quantified Boolean Formulas; 2.3 Dependency Quantified Boolean Formulas; 2.4 From Circuits to Formulas; 3 Unknown Values in Circuit Test; 3.1 Standard X-Logic Simulation; 3.2 Accurate Logic Simulation; 3.3 Accurate Fault Simulation 000727549 506__ $$aAccess limited to authorized users. 000727549 520__ $$aThis book presents the lecture notes of the 1st Summer School on Methods and Tools for the Design of Digital Systems, 2015, held in Bremen, Germany. The topic of the summer school was devoted to modeling and verification of cyber-physical systems. This covers several aspects of the field, including hybrid systems and model checking, as well as applications in robotics and aerospace systems. The main chapters have been written by leading scientists, who present their field of research, each providing references to introductory material as well as latest scientific advances and future research. 000727549 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed June 10, 2015). 000727549 650_0 $$aFormal methods (Computer science)$$vCongresses. 000727549 650_0 $$aEmbedded computer systems$$vCongresses. 000727549 650_0 $$aUbiquitous computing$$vCongresses. 000727549 7001_ $$aDrechsler, Rolf,$$eeditor. 000727549 7001_ $$aKühne, Ulrich,$$eeditor. 000727549 77608 $$iPrint version:$$aDrechsler, Rolf$$tFormal Modeling and Verification of Cyber-Physical Systems : 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015$$dWiesbaden : Springer Fachmedien Wiesbaden,c2015$$z9783658099930 000727549 852__ $$bebk 000727549 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-658-09994-7$$zOnline Access$$91397441.1 000727549 909CO $$ooai:library.usi.edu:727549$$pGLOBAL_SET 000727549 980__ $$aEBOOK 000727549 980__ $$aBIB 000727549 982__ $$aEbook 000727549 983__ $$aOnline 000727549 994__ $$a92$$bISE