Dependable Software Engineering. Theories, Tools, and Applications
5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings
Published on 18. November 2019
XIII, 139 pages
978-3-030-35540-1 (ISBN)
Description
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 cutting-edge advancements in the field of formal methods and its interoperability with software engineering and focus on the application of formal techniques and tools for building reliable, safe, secure, and smart systems with multi-dimensional complexities.
The 8 full papers presented were carefully reviewed and selected from 26 submissions. They present cutting-edge advancements in the field of formal methods and its interoperability with software engineering and focus on the application of formal techniques and tools for building reliable, safe, secure, and smart systems with multi-dimensional complexities.
More details
Series
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Product notice
Reflowable
Illustrations
XIII, 139 p. 135 illus., 23 illus. in color.
File size
10,07 MB
ISBN-13
978-3-030-35540-1 (9783030355401)
DOI
10.1007/978-3-030-35540-1
Schweitzer Classification
Other editions
Additional editions
Nan Guan | Joost-Pieter Katoen | Jun Sun
Dependable Software Engineering. Theories, Tools, and Applications
5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings
Book
11/2019
Springer
€53.49
Shipment within 7-9 days
Content
- 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 Optimization
- 4.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 Introduction
- 2 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 Development
- 2.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 Contribution
- 2 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
- 1 Introduction
- 2 Background and Related Work
- 2.1 TLSF Algorithm
- 2.2 Related Work
- 3 The Data Structure and Configuration
- 3.1 System Configuration
- 3.2 System State
- 3.3 Bitmap Matrix
- 4 Formalizing the Abstract Specification
- 4.1 Invariants
- 4.2 Specification of Allocation
- 4.3 Specification of Deallocation
- 5 Formalizing the Algorithm
- 5.1 State Monads
- 5.2 Formal Specification of Memory Functions
- 6 Formal Verification and Results
- 6.1 Verification Using State Monad
- 6.2 Evaluation
- 7 Conclusion
- References
- Author Index
