國立高雄大學圖資館 |

Language: English

Back

Formal verification of Simulink/Stat...

SpringerLink (Online service)

Formal verification of Simulink/Stateflow diagramsa deductive approach /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Formal verification of Simulink/Stateflow diagramsby Naijun Zhan, Shuling Wang, Hengjun Zhao.
Reminder of title:	a deductive approach /
Author:	Zhan, Naijun.
other author:	Wang, Shuling.
Published:	Cham :Springer International Publishing :2017.
Description:	xv, 258 p. :ill., digital ;24 cm.
Contained By:	Springer eBooks
Subject:	Computer softwareVerification.
Online resource:	http://dx.doi.org/10.1007/978-3-319-47016-0
ISBN:	9783319470160$q(electronic bk.)

Formal verification of Simulink/Stateflow diagramsa deductive approach /
Zhan, Naijun.

Formal verification of Simulink/Stateflow diagramsa deductive approach /[electronic resource] :by Naijun Zhan, Shuling Wang, Hengjun Zhao. - Cham :Springer International Publishing :2017. - xv, 258 p. :ill., digital ;24 cm.

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

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

ISBN: 9783319470160$q(electronic bk.)

Standard No.: 10.1007/978-3-319-47016-0doiSubjects--Uniform Titles:

SIMULINK.
Subjects--Topical Terms:

184731
Computer software
--Verification.

LC Class. No.: QA76.76.V47

Dewey Class. No.: 005.14

Formal verification of Simulink/Stateflow diagramsa deductive approach /
LDR:02349nmm a2200313 a 4500 001 505671
003 DE-He213
005 20170614093331.0
006 m d
007 cr nn 008maaau
008 171030s2017 gw s 0 eng d
020 $a 9783319470160$q(electronic bk.)
020 $a 9783319470146$q(paper)
024 7 $a 10.1007/978-3-319-47016-0 $2 doi
035 $a 978-3-319-47016-0
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.76.V47
072 7 $a TJFC $2 bicssc
072 7 $a TEC008010 $2 bisacsh
082 0 4 $a 005.14 $2 23
090 $a QA76.76.V47 $b Z63 2017
100 1 $a Zhan, Naijun. $3 761281
245 1 0 $a Formal verification of Simulink/Stateflow diagrams $h [electronic resource] : $b a deductive approach / $c by Naijun Zhan, Shuling Wang, Hengjun Zhao.
260 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2017.
300 $a xv, 258 p. : $b ill., digital ; $c 24 cm.
505 0 $a 1 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 $a This 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.
630 0 0 $a SIMULINK. $3 182730
630 0 0 $a Stateflow. $3 489475
650 0 $a Computer software $x Verification. $3 184731
650 1 4 $a Engineering. $3 210888
650 2 4 $a Circuits and Systems. $3 274416
650 2 4 $a Processor Architectures. $3 274498
650 2 4 $a Electronic Circuits and Devices. $3 495609
700 1 $a Wang, Shuling. $3 771157
700 1 $a Zhao, Hengjun. $3 771158
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer eBooks
856 4 0 $u http://dx.doi.org/10.1007/978-3-319-47016-0
950 $a Engineering (Springer-11647)