Dependable software engineering : theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings /: theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings. (2019)

• Record Type: Book
• Other Titles: SETTA 2019
• Further Information: Note: Nan Guan, Joost-Pieter Katoen, Jun Sun (eds.).
• Editors: Guan, Nan; Katoen, Joost-Pieter; (Professor of Information Systems), Sun, Jun
• Other Names: SETTA (Symposium), 5th
• Contents: Intro; Preface; Organization; Abstracts; The Rise of Model Counting: A Child of SAT Revolution; Building and Updating Safety-Critical Embedded Systems with Deterministic Timing and Functional Behaviours; Contents; A Bounded Model Checking Technique for Higher-Order Programs; 1 Introduction; 2 The Language: HORef; 3 A Bounded Translation for HORef; 4 A Points-To Analysis for Names; 5 Implementation and Experiments; References; Fault Trees from Data: Efficient Learning with an Evolutionary Algorithm; 1 Introduction; 2 Related Work; 3 Background 4 Learning Fault Trees with Nature-Inspired Stochastic Optimization4.1 Initialization; 4.2 Mutation and Recombination; 4.3 Evaluation; 4.4 Selection; 4.5 Termination; 5 Learning of Partial Fault Trees; 5.1 Initialization; 5.2 Mutation and Recombination; 6 Experimental Evaluation; 6.1 Experimental Set Up; 6.2 Synthetic Dataset: Accuracy and Runtime; 6.3 Synthetic Dataset: Other Statistics; 6.4 Case Study with Industrial Dataset; 6.5 Fault Tree Benchmark; 7 Discussion; 8 Conclusion and Future Work; References; Simplifying the Analysis of Software Design Variants with a Colorful Alloy 1 Introduction2 Overview; 3 Language; 4 Analysis; 5 Evaluation; 5.1 Evaluation Subjects; 5.2 Results; 6 Related Work; 7 Conclusion and Future Work; References; Response Time Analysis of Typed DAG Tasks for G-FP Scheduling; 1 Introduction; 2 Related Work; 3 Preliminaries; 4 Rationale; 4.1 Bounding Intra-interference; 5 Bounding Inter-interference; 5.1 Bounding Carry-In Interference; 5.2 Bounding Carry-Out Interference; 6 Schedulability Analysis; 7 Evaluation; 8 Conclusion; References; A Formal Modeling and Verification Framework for Flash Translation Layer Algorithms; 1 Introduction 2 Informal Development2.1 Modeling FTL Algorithms; 2.2 Correctness Requirement of FTL Algorithms; 2.3 Our Proof Technique Based on Invariant; 3 Modeling FTL and Its Functional Correctness; 3.1 Disk Device; 3.2 Flash Device and FTL; 3.3 The Correctness Definition of FTL; 4 Verification Framework; 5 Case Study: Verifying an FTL Algorithm BAST; 5.1 Overview of BAST; 5.2 The Global Invariant for BAST; 5.3 Mechanized Proof and Experience; 6 Related Work and Conclusion; 7 Conclusion; References; Mixed Criticality Scheduling of Probabilistic Real-Time Systems; 1 Introduction 1.1 Problem Discussion and Contribution2 Notations and Definitions; 2.1 Computational Model; 3 Probabilistic Scheduling Model; 3.1 Graph Model; 3.2 Scheduling Tree; 4 Evaluation; 5 Conclusion; References; Improving the Analysis of GPC in Real-Time Calculus; 1 Introduction; 2 RTC Basics; 2.1 Arrival and Service Curves; 2.2 Greedy Processing Component (GPC); 3 Revised Proof of Output Curves; 4 Improving Output Arrival Curves; 5 Experiments; 5.1 Parameter Setting I; 5.2 Parameter Setting II; 6 Conclusion; References; A Verified Specification of TLSF Memory Management Allocator Using State Monads
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2019
• Extent: 1 online resource (xiii, 139 pages), illustrations (some color)
• Subjects: 005.1; Software engineering -- Congresses; Electronic books; Electronic books
• Languages: English
• ISBNs: 9783030355401; 3030355403
• Related ISBNs: 9783030355395
• Notes: Note: Includes bibliographical references and author index.; Note: Online resource; title from PDF title page (SpringerLink, viewed November 20, 2019).
• 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.