Software Engineering and Formal Methods

Name: Software Engineering and Formal Methods | 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings

Alessandro Cimatti Marjan Sirjani(Herausgeber*in)

Springer (Verlag)

Erschienen am 24. August 2017

XIX, 410 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-66197-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
Invited Talks
The Challenge of Change
Software Safety and Security, Assurance Cases and Model Management
A Formal Contract-Based Design Methodology for CyberPhysical Systems
Contents
Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory
1 Introduction
2 Evading Existing Information Flow Trackers
2.1 Exploiting a Race Condition to Copy a File Without Its Taint
2.2 Making a Flow in Memory
3 A New Algorithm for Taint Propagation
3.1 Tags, Information Flows and Executions
3.2 Flow-Based Interpretations of Executions
4 Implementation and Experiments
5 Related Work
6 Conclusion
References
Focused Certification of an Industrial Compilation and Static Verification Toolchain
1 Introduction
2 Technical Approach
2.1 Core SPARK 2014 Mechanized Semantics
2.2 Certified Run-Time Check Generator
2.3 Certified Run-Time Check Optimizer
2.4 Certifying GNAT RT Check Generator
3 Evaluation: Certifying GNAT
4 Related Work
5 Conclusions and Future Work
References
A Complete Generative Label Model for Lattice-Based Access Control Models
1 Introduction
2 Overview of Denning's Lattice Model
3 Recasting Denning's Model via Semantic Labels
3.1 Illustration of the Recasting Procedure Through Examples
4 Recasting Readers/Writers Explicitly in Labels
4.1 Basic Readers Writers Flow Model (B-RWFM)
4.2 Characteristic Properties of B-RWFM
5 Encoding Common Security Policies in RWFM
6 Where does RWFM stand in relation to RBAC
7 Conclusions
References
From Model Checking to a Temporal Proof for Partial Models
1 Introduction
2 Background
3 THRIVE
4 Using THRIVE with PKS and LTL
4.1 Adapting the Theorem Prover
4.2 Integrating the Model Checker and the Theorem Prover
4.3 Thorough Semantics and THRIVE
5 Preliminary Evaluation
6 Using THRIVE in Real Cases
7 Conclusions and Future Work
References
Modeling and Reasoning on Requirements Evolution with Constrained Goal Models
1 Introduction
2 Background: Constrained Goal Models
3 Requirements Evolution and Evolution Requirements
3.1 Requirements Evolution
3.2 Evolution Requirements
4 Automated Reasoning with Evolution Requirements
5 Implementation
6 Conclusions
References
Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL
1 Introduction
2 Approach to Participatory Verification for Railway Regulations
3 RailCNL: A Front-End Language for Railway Verification
3.1 RailCNL Grammar
3.2 RailCNL Modules and Examples
3.3 Translating RailCNL into Datalog
3.4 Tool Integration
4 Design Methodology for a Verification Front-End Language
4.1 Abstract Syntax
4.2 Concrete Syntax
4.3 Translation into the Target Logic Formalism
5 Evaluation and Conclusions
References
An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions
1 Introduction
2 Preliminaries
2.1 Kripke Structures, Regular Expressions, and Finite Automata
2.2 The Interval Temporal Logic HS
3 The General Picture
4 MC for Full HS
5 Exponential Small-Model for AABB and AAEE
6 PSPACE-Completeness of MC for AABB
7 Conclusions
References
PARTPW: From Partial Analysis Results to a Proof Witness
1 Introduction
2 Background
3 When Do Partial ARGs Witness Program Safety?
4 Proof Witnesses from Complete Sets of Partial ARGs
5 Experiments
6 Conclusion
References
Specification and Automated Verification of Dynamic Dataflow Networks
1 Introduction
2 Dataflow Actors and Networks
3 Verification Technique
3.1 Networks
3.2 Actors
4 Programming and Assertion Language
5 Encoding
5.1 Assertions
5.2 Basic Actors
5.3 Networks
6 Invariant Generation
7 Soundness
8 Evaluation
9 Related Work
10 Conclusion
References
Specification Clones: An Empirical Study of the Structure of Event-B Specifications
1 Introduction and Motivation
2 Background and Related Work
2.1 Clones in Code and Specifications
2.2 Modularisation of Event-B Specifications
3 Analysing a Corpus of Event-B Specifications: Metrics and Refinement
3.1 Quantifying Specification Size
3.2 Metrics for Event-B Specifications
3.3 Quantifying Refinements
4 Detecting Specification Clones
5 Results of the Clone Analysis
5.1 Context Clones
5.2 Machine Clones
5.3 Event Clones
5.4 Discussion: Dealing with Clones
6 Threats to Validity
7 Summary and Future Work
References
User Studies of Principled Model Finder Output
1 Introduction
2 Principled Output Methods Being Evaluated
2.1 Minimality and Maximality
2.2 UNSAT Cores
2.3 Provenance
3 Evaluation with Student Subjects
3.1 Minimality and Maximality
3.2 UNSAT Cores
3.3 Provenance
3.4 Discussion
4 Evaluation with Crowd-Sourced Subjects
4.1 Design Decisions
4.2 Training Crowd Workers in Formal Methods
4.3 Effects of Unsat Cores and Provenance
4.4 Discussion
5 Related Work
6 Conclusion
References
Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models
1 Introduction
2 Weak Memory Models
3 Multi-threaded Programs over Shared Memory Abstractions
4 Verification with Thread-Asynchronous SMAs
5 Individual Memory-Location Unwindings
6 IMU-based SMA Implementations
7 Experimental Evaluation
8 Related Work, Conclusions, and Future Work
References
On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows
1 Introduction
2 Background
3 A Catalog of Authorization Constraints
3.1 Classification of Constraints
3.2 Data-Based Constraints
4 Encoding Constraints in Cerberus
4.1 Overview of Cerberus
4.2 Run-Time Monitor Synthesis
4.3 Encoding Constraints
5 Conclusion
References
Trace Partitioning and Local Monitoring for Asynchronous Components
1 Introduction
2 Monitors and Specification
3 The Approach
4 The Implementability of Local Monitoring
5 Experimental Evaluation
5.1 Monitoring for the Ranch Connection Protocol
5.2 Experiment Set-Up and Design
5.3 Results and Analysis
6 Conclusion
References
Compositional Verification of Interlocking Systems for Large Stations
1 Introduction
2 Interlocking Systems and Their Verification
3 Compositionality
4 Horizontal Cut
4.1 Decomposition of the Network
4.2 Decomposition of the Interlocking Table
4.3 Safety Verification
4.4 Soundness of the Approach
5 A More Complex Example
6 Conclusions
References
Formalizing Timing Diagram Requirements in Discrete Duration Calculus
1 Introduction
2 Logic QDDC
2.1 Chop Expressions: Ce and SeCe
2.2 DCVALID and DCSynth
2.3 Logic SeCeNL: Syntax and Semantics
3 Formalizing Timing Diagrams
3.1 Waveform to SeCeNL Translation
3.2 Comparision with Other Temporal Logics
4 Case Study: Minepump Specification
References
On Approximate Diagnosability of Metric Systems
1 Introduction
2 Notation and Preliminary Definitions
3 Metric Systems
4 Approximate Diagnosability
5 Approximate Simulation and Diagnosability
6 Application to Diagnosability of Nonlinear Systems
7 Conclusions
References
A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices
1 Introduction
2 Background on STPA
3 Enhanced STPA Analysis
3.1 New Causal Factor Categories
3.2 Process for Using the New Categories
4 Case Study: The Gantry-2 System
5 Formalization of Safety Requirements in PVS
5.1 Gantry-2 Model in PVS
5.2 Formalization of the Requirements
6 Related Work
7 Conclusion
References
Modular Verification of Information Flow Security in Component-Based Systems
1 Introduction
2 Formal Framework
2.1 Components and Services
2.2 Non-interference
3 Service-Local Non-interference Specification
4 Dependency Clusters and Components
5 Weakening Specifications
6 Proof of Concept: Verifying JavaEE Implementations
7 Conclusion
References
IJIT: An API for Boolean Program Analysis with Just-in-Time Translation
1 Introduction
2 Boolean Programs and Thread-Transition Systems
2.1 Boolean Programs
2.2 From Boolean Programs to Thread Transition Systems
3 BP Analysis with JIT Translation: Overview
4 The IJIT Application Programming Interface
4.1 API Usage
4.2 API Design
5 Case Study: Performance Benefits of IJIT
5.1 Benchmark Algorithms
5.2 Case Study
6 Related Work
7 Summary
References
Specification and Semantic Analysis of Embedded Systems Requirements: From Description Logic to Temporal Logic
1 Introduction
2 Preliminaries
2.1 ReSA
2.2 Description Logic
2.3 Timed Computation Tree Logic
3 Defining ReSA Semantics in DL
3.1 Semantic Analysis Framework
3.2 Semantic Representation via the Event-Based Approach
3.3 The ReSA Ontology
3.4 Semantics of Clauses and Statements in ReSA
4 Semantic Equivalence in ReSA
5 Automated Analysis and Transformation to TCTL Properties
5.1 Consistency Checking
5.2 Completeness
5.3 Transformation to TCTL
6 Related Work
7 Conclusions
References
Computing Conditional Probabilities: Implementation and Evaluation
1 Introduction
2 Preliminaries
3 Implementation
4 Evaluation and Comparative Studies
4.1 Methodology
4.2 Considered Models and Properties
4.3 Results
5 Comparison Prism vs Storm
6 Conclusion
References
Validating the Meta-Theory of Programming Languages (Short Paper)
1 Introduction
2 Binders-Aware Property-Based Testing
3 Experiments
4 Conclusions and Future Work
References
Towards Inverse Uncertainty Quantification in Software Development (Short Paper)
1 Introduction
2 Overview of the Approach
3 Related Work
4 Conclusion
References
Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper)
1 Introduction
2 Background
2.1 Model, Notation and Property Definition
2.2 Bounded Model Checking
2.3 Craig Interpolants
3 Combining SAT-based BMC and Interpolation
4 Experimental Results
5 Conclusions
References
Towards Automated Deployment of Self-adaptive Applications on Hybrid Clouds (Short Paper)
1 Introduction
2 Related Work and Background
3 Outline of the Solution
4 Real-World Trials
References
A Diagnosis Framework for Critical Systems Verification (Short Paper)
1 Introduction
2 Background
3 Conceptual Framework
3.1 Activities
3.2 Propositional Objects
3.3 Associations
4 Framework by Example
5 Conclusion
References
Design of Embedded Systems with Complex Task Dependencies and Shared Resource Interference (Short Paper)
1 Introduction
2 Fixed Priority Process Networks
3 Design and Scheduling for FPPNs in TASTE
4 Case-Study: Guidance Navigation Control Application
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken