000 03444nam a22005295i 4500
001 978-3-319-47016-0
003 DE-He213
005 20220801222527.0
007 cr nn 008mamaa
008 161107s2017 sz | s |||| 0|eng d
020 _a9783319470160
_9978-3-319-47016-0
024 7 _a10.1007/978-3-319-47016-0
_2doi
050 4 _aTK7867-7867.5
072 7 _aTJFC
_2bicssc
072 7 _aTEC008010
_2bisacsh
072 7 _aTJFC
_2thema
082 0 4 _a621.3815
_223
100 1 _aZhan, Naijun.
_eauthor.
_0(orcid)0000-0003-3298-3817
_1https://orcid.org/0000-0003-3298-3817
_4aut
_4http://id.loc.gov/vocabulary/relators/aut
_961958
245 1 0 _aFormal Verification of Simulink/Stateflow Diagrams
_h[electronic resource] :
_bA Deductive Approach /
_cby Naijun Zhan, Shuling Wang, Hengjun Zhao.
250 _a1st ed. 2017.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2017.
300 _aXV, 258 p. 74 illus., 60 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
505 0 _a1 Introduction -- 2 Preliminaries -- 3 Unifying Theories of Programming -- 4 Simulink -- 5 Stateflow and Its Combination with Simulink -- 6 Hybrid CSP -- 7 Hybrid Hoare Logic -- 8 The HHL Prover -- 9 Invariant Generation -- 10 Translating Simulink Diagrams into HCSP -- 11 Translating Simulink/Stateflow Diagrams into HCSP -- 12 From HCSP to Simulink -- 13 MARS A Toolkit for Modelling, Analysis and Verification of Hybrid Systems -- 14 Case Studies.
520 _aThis book presents a state-of-the-art technique for formal verification of continuous-time Simulink/Stateflow diagrams, featuring an expressive hybrid system modelling language, a powerful specification logic and deduction-based verification approach, and some impressive, realistic case studies. Readers will learn the HCSP/HHL-based deductive method and the use of corresponding tools for formal verification of Simulink/Stateflow diagrams. They will also gain some basic ideas about fundamental elements of formal methods such as formal syntax and semantics, and especially the common techniques applied in formal modelling and verification of hybrid systems. By investigating the successful case studies, readers will realize how to apply the pure theory and techniques to real applications, and hopefully will be inspired to start to use the proposed approach, or even develop their own formal methods in their future work.
650 0 _aElectronic circuits.
_919581
650 0 _aMicroprocessors.
_961959
650 0 _aComputer architecture.
_93513
650 1 4 _aElectronic Circuits and Systems.
_961960
650 2 4 _aProcessor Architectures.
_961961
700 1 _aWang, Shuling.
_eauthor.
_4aut
_4http://id.loc.gov/vocabulary/relators/aut
_961962
700 1 _aZhao, Hengjun.
_eauthor.
_4aut
_4http://id.loc.gov/vocabulary/relators/aut
_961963
710 2 _aSpringerLink (Online service)
_961964
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783319470146
776 0 8 _iPrinted edition:
_z9783319470153
776 0 8 _iPrinted edition:
_z9783319836386
856 4 0 _uhttps://doi.org/10.1007/978-3-319-47016-0
912 _aZDB-2-ENG
912 _aZDB-2-SXE
942 _cEBK
999 _c80865
_d80865