Formal Verification of Simulink/Stateflow Diagrams A Deductive Approach /

• Κύριοι συγγραφείς: Zhan, Naijun (Συγγραφέας), Wang, Shuling (Συγγραφέας), Zhao, Hengjun (Συγγραφέας)
• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Cham : Springer International Publishing : Imprint: Springer, 2017.
• Θέματα: Engineering.; Microprocessors.; Electronic circuits.; Circuits and Systems.; Processor Architectures.; Electronic Circuits and Devices.

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

Πίνακας περιεχομένων:

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