Dependable software engineering : theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings / Nan Guan, Joost-Pieter Katoen, Jun Sun (eds.)
This book constitutes the proceedings of the 5th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2019, held in Shanghai, China, in November 2019. The 8 full papers presented were carefully reviewed and selected from 26 submissions. They present cu...
Saved in:
| Online Access: |
Full Text (via Springer) |
|---|---|
| Corporate Author: | |
| Other Authors: | , , |
| Other title: | SETTA 2019. |
| Format: | Conference Proceeding eBook |
| Language: | English |
| Published: |
Cham, Switzerland :
Springer,
2019.
|
| Series: | Lecture notes in computer science ;
11951. LNCS sublibrary. Programming and software engineering. |
| Subjects: |
Table of 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.