Formal techniques for safety-critical systems : 7th International Workshop, FTSCS 2019, Shenzhen, China, November 9, 2019, Revised selected papers /: 7th International Workshop, FTSCS 2019, Shenzhen, China, November 9, 2019, Revised selected papers. (2020)

• Record Type: Book
• Other Titles: FTSCS 2019
• Further Information: Note: Osman Hasan, Frédéric Mallet (eds.).
• Editors: Hasan, Osman, 1975-; Mallet, Frédéric
• Other Names: FTSCS (Workshop), 7th
• Contents: Intro -- Preface -- Organization -- Contents -- Invited Paper -- Formal Verification of Cyber-Physical Systems Using Theorem Proving -- 1 Introduction -- 2 Formal Functional Analysis -- 2.1 Verification of Physical Components -- 2.2 Verification of Software Components -- 2.3 Verification of Control and Signal Processing Components -- 2.4 Formal Hybrid Analysis -- 3 Formal Probabilistic and Performance Analysis -- 4 Formal Dependability Analysis -- 5 Theorem Proving Support for CPS -- 6 Conclusion -- References -- Avionics and Spacecraft Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661 -- 1 Introduction -- 2 Preliminaries -- 2.1 The Modelling Framework: Event-B -- 2.2 ICO Notation and PetShop CASE Tool -- 3 FLUID Language -- 4 MPIA Case Study -- 5 Formal Development of MPIA in FLUID -- 5.1 Declaration -- 5.2 State -- 5.3 Events -- 5.4 Requirements -- 6 Exploring the MPIA FLUID Model in Event-B -- 6.1 Model -- 6.2 Model Validation and Analysis -- 7 Exploring the MPIA FLUID Model in PetShop -- 8 Assessment -- 9 Related Work -- 10 Conclusion -- References Verifying Resource Adequacy of Networked IMA Systems at Concept Level -- 1 Introduction -- 2 Background -- 3 Methodology -- 3.1 Overall Network Architecture -- 3.2 System Global Declarations -- 3.3 Timed Automata Templates -- 4 Requirement Specification -- 4.1 Requirement Definition -- 4.2 Verifying Requirements in UPPAAL -- 4.3 Expressing Requirements in UPPAAL -- 5 Model Assessment -- 6 Conclusions -- References -- Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study -- 1 Introduction -- 2 Preliminary -- 2.1 SIGNAL -- 2.2 S-CGA 3 Ada Code Generation Approach -- 3.1 Dependency Analysis and Task Partition -- 3.2 Platform-Independent Level: VMT Generation -- 3.3 Platform-Dependent Level: Ada Code Generation -- 4 Industrial Case Study -- 4.1 Code Generation of Data Processing of Sun Sensor -- 4.2 Strategies Comparisons -- 4.3 Threat to Validity -- 5 Lessons Learnt and Discussions -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Applications -- POP: A Tuning Assistant for Mixed-Precision Floating-Point Computations -- 1 Introduction -- 2 Overview -- 3 Preliminary Notions 3.1 Basics on Floating-Point Arithmetic -- 3.2 Related Work -- 4 Static Analysis by Constraints Generation -- 4.1 Forward and Backward Error Analysis -- 4.2 Constraints Generation -- 5 The POP Tool -- 5.1 Architecture -- 5.2 Simple Imperative Language of Constraints -- 6 Experimental Results -- 7 Conclusions and Future Work -- References -- Visualising Railway Safety Verification -- 1 Introduction -- 2 Related Work -- 2.1 Railway Verification -- 2.2 Graph Layout for Railways -- 2.3 Dynamic Data Visualisation -- 3 Railway Visualisation Methods -- 3.1 The Simulated Annealing Layout Algorithm
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2020
• Extent: 1 online resource (viii, 141 pages), illustrations (some color)
• Subjects: 004.01/51; Formal methods (Computer science) -- Congresses; System safety -- Congresses; Systems engineering -- Congresses; Formal methods (Computer science); System safety; Systems engineering; Electronic books; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783030469023; 3030469026
• Related ISBNs: 9783030469016; 3030469018
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed May 4, 2020).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.