Dependable Software Engineering. Theories, Tools, and Applications

Name: Dependable Software Engineering. Theories, Tools, and Applications | 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings

Nan Guan Joost-Pieter Katoen Jun Sun(Herausgeber*in)

Springer (Verlag)

Erschienen am 18. November 2019

XIII, 139 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-35540-1 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken