000779942 000__ 06240cam\a2200553Ii\4500
000779942 001__ 779942
000779942 005__ 20230306143046.0
000779942 006__ m\\\\\o\\d\\\\\\\\
000779942 007__ cr\nn\nnnunnun
000779942 008__ 170303s2017\\\\sz\a\\\\o\\\\\000\0\eng\d
000779942 019__ $$a974697071$$a974765558$$a974959491$$a975022881$$a975131325$$a975425354$$a984870935
000779942 020__ $$a9783319486284$$q(electronic book)
000779942 020__ $$a3319486284$$q(electronic book)
000779942 020__ $$z9783319486277
000779942 020__ $$z3319486276
000779942 0247_ $$a10.1007/978-3-319-48628-4$$2doi
000779942 035__ $$aSP(OCoLC)ocn974489154
000779942 035__ $$aSP(OCoLC)974489154$$z(OCoLC)974697071$$z(OCoLC)974765558$$z(OCoLC)974959491$$z(OCoLC)975022881$$z(OCoLC)975131325$$z(OCoLC)975425354$$z(OCoLC)984870935
000779942 040__ $$aN$T$$beng$$erda$$epn$$cN$T$$dGW5XE$$dN$T$$dIDEBK$$dEBLCP$$dYDX$$dOCLCF$$dUAB$$dIOG$$dCOO$$dAZU$$dUPM
000779942 049__ $$aISEA
000779942 050_4 $$aQA76.76.V47
000779942 08204 $$a005.1/4$$223
000779942 24500 $$aProvably correct systems /$$cMike Hinchey, Jonathan P. Bowen, Ernst-Rüdiger Olderog, editors.
000779942 264_1 $$aCham, Switzerland :$$bSpringer,$$c2017.
000779942 300__ $$a1 online resource (xviii, 328 pages) :$$billustrations.
000779942 336__ $$atext$$btxt$$2rdacontent
000779942 337__ $$acomputer$$bc$$2rdamedia
000779942 338__ $$aonline resource$$bcr$$2rdacarrier
000779942 347__ $$atext file$$bPDF$$2rda
000779942 4901_ $$aNASA monographs in systems and software engineering,$$x1860-0131
000779942 5050_ $$aForeword; Preface; Impact; Structure of this Book; Historic Account; Hybrid Systems; Correctness of Concurrent Algorithms; Interfaces and Linking; Automatic Verification; Run-Time Assertion Checking; Formal and Semi-formal Methods; Web-Supported Communities in Science; Acknowledgements; Contents; Part I Historic Account; ProCoS: How It All Began -- as Seen from Denmark; Part II Hybrid Systems; Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systems; 1 Introduction; 2 Stochastic Hybrid Transition Systems; 3 Bounded Reachability Checking for Stochastic Hybrid Automata
000779942 5058_ $$a3.1 Stochastic Satisfiability Modulo Theory3.2 CSSMT Solving; 4 Parameter Synthesis for Parametric Stochastic Hybrid Automata; 4.1 Parameter Synthesis Using Symbolic Importance Sampling; 5 Conclusion; References; MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems; 1 Introduction; 1.1 Related Work; 2 Sim2HCSP Translator; 3 HHL Prover; 4 Invariant Generator; 4.1 Isabelle Oracle; 4.2 Differential Invariant Generation; 4.3 Abstraction of Elementary Hybrid Systems by Variable Transformation; 4.4 QE-Based Invariant Generator; 4.5 SOS-Based Invariant Generator
000779942 5058_ $$a5 Conclusion and Future WorkReferences; Part III Correctness of Concurrent Algorithms; A Proof Method for Linearizability on TSO Architectures; 1 Introduction; 2 Linearizability; 2.1 A Formal Definition of Linearizability; 2.2 A Proof Method for Linearizability; 3 The TSO Memory Model; 3.1 TSO-Linearizability; 4 Using a Coarse-Grained Abstraction; 4.1 Defining the Coarse-Grained Abstraction; 4.2 From Coarse-Grained to Abstract Specification; 5 Case Study: Work-Stealing Deque; 5.1 Abstract Specification; 5.2 Concrete Specification; 5.3 Refined Abstract Specification
000779942 5058_ $$a5.4 Coarse-Grained Abstraction6 Conclusion; References; Part IV Interfaces and Linking; Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers; 1 Introduction; 2 Symbolic Model; 2.1 View; 2.2 Spatial Logic; 2.3 Transition System; 3 Abstract Controllers; 3.1 Keeping Distance; 3.2 Changing Lanes; 3.3 Safety; 4 Concrete Model; 4.1 Longitudinal Motion; 4.2 Lateral Motion; 5 Linking; 5.1 Distance Controller; 5.2 Lane-Change Controller; 6 Concrete Controllers; 6.1 Longitudinal Control; 6.2 Lane Change; 7 Related Work; 8 Conclusion; References
000779942 5058_ $$aTowards Interface-Driven Design of Evolving Component-Based Architectures1 Introduction; 2 Complex Evolving Systems; 2.1 Chronic Complexity of Digital Ecosystems; 2.2 An Application Examples; 3 Interfaces and Component-Based Architectures; 3.1 Key Features of rCOS; 3.2 Components and Their Interfaces; 3.3 Composition and Orchestration; 3.4 Separation of Concerns; 4 Incremental Design of an Enterprise Application; 4.1 Requirements Modelling; 4.2 OO Design of Components; 4.3 Incremental Development and System Evolution; 5 Towards Modelling Cyber-Physical Component Systems
000779942 506__ $$aAccess limited to authorized users.
000779942 520__ $$aAs computers increasingly control the systems and services we depend upon within our daily lives like transport, communications, and the media, ensuring these systems function correctly is of utmost importance. This book consists of twelve chapters and one historical account that were presented at a workshop in London in 2015, marking the 25th anniversary of the European ESPRIT Basic Research project ‘ProCoS’ (Provably Correct Systems). The ProCoS I and II projects pioneered and accelerated the automation of verification techniques, resulting in a wide range of applications within many trades and sectors such as aerospace, electronics, communications, and retail. The following topics are covered: An historical account of the ProCoS project Hybrid Systems Correctness of Concurrent Algorithms Interfaces and Linking Automatic Verification Run-time Assertions Checking Formal and Semi-Formal Methods <web-supported scientific="" communities Provably Correct Systems provides researchers, designers and engineers with a complete overview of the ProCoS initiative, past and present, and explores current developments and perspectives within the field.
000779942 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed March 9, 2017).
000779942 650_0 $$aComputer software$$xVerification.
000779942 650_0 $$aEmbedded computer systems.
000779942 7001_ $$aHinchey, Michael G.$$q(Michael Gerard),$$d1969-$$eeditor.
000779942 7001_ $$aBowen, J. P.$$q(Jonathan Peter),$$d1956-$$eeditor.
000779942 7001_ $$aOlderog, E.-R.,$$eeditor.
000779942 77608 $$iPrint version:$$z3319486276$$z9783319486277$$w(OCoLC)959592854
000779942 830_0 $$aNASA monographs in systems and software engineering.
000779942 852__ $$bebk
000779942 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-319-48628-4$$zOnline Access$$91397441.1
000779942 909CO $$ooai:library.usi.edu:779942$$pGLOBAL_SET
000779942 980__ $$aEBOOK
000779942 980__ $$aBIB
000779942 982__ $$aEbook
000779942 983__ $$aOnline
000779942 994__ $$a92$$bISE