| 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 |
||