de
en
Schliessen
Detailsuche
Bibliotheken
Projekt
Impressum
Datenschutz
Schliessen
Publizieren
Besondere Sammlungen
Digitalisierungsservice
Hilfe
Impressum
Datenschutz
zum Inhalt
Detailsuche
Schnellsuche:
OK
Ergebnisliste
Titel
Titel
Inhalt
Inhalt
Seite
Seite
Im Werk suchen
Knowledge-based verification of service compositions / vorgelegt von Sven Walther. Paderborn, 2018
Inhalt
List of Figures
List of Tables
1 Introduction
1.1 A Theoretical Framework
1.2 A Practical Implementation
1.3 Structure of this Thesis
I Preliminaries
2 Domain Knowledge and Logic
2.1 Formalizing Domain Knowledge
2.2 Description Logics, Ontologies, and Knowledge Bases
2.2.1 Description Logics as Ontology Semantics
2.2.2 Reasoning in DLs: General Concept Inclusion
2.2.3 Higher-level Ontology Languages
2.2.4 Enhancing Ontologies with Rules
2.2.5 A Formal Knowledge Base
II Contributions
3 Workflow Descriptions
3.1 Related Work
3.2 Syntax and Semantics
3.2.1 Services and Service Compositions
3.2.2 States, Configurations, and Semantics of Workflows
3.3 Partial and Total Correctness
3.4 Proof Calculus
3.4.1 Axioms and Rules
3.4.2 Soundness
3.4.3 Completeness
4 Workflow Templates
4.1 Related Work
4.2 Syntax and Semantics
4.3 Partial and Total Correctness
4.4 Proof Calculus
4.4.1 Axioms and Rules
4.4.2 Soundness and Completeness
4.5 Correct Instantiations
4.5.1 Ontology Mappings
4.5.2 Template Instantiation
4.5.3 Correctness by Construction
5 Automating Correctness Proofs using First-order Logic
5.1 Related Work and the Treatment of Loops
5.2 First-order Logic Encodings
5.2.1 Preliminaries
5.2.2 Domain Knowledge and Services
5.2.3 Control Flow
5.3 Correspondence of Correctness and Sat Problems
5.3.1 Correspondence Theorem
5.3.2 Proofs
5.4 Deriving Invariants and Termination Functions
5.4.1 Finding Loop Invariants using Domain Knowledge
5.4.2 Finding Termination Functions using Domain Knowledge
6 Dealing with Uncertain Service Descriptions
6.1 Uncertainty in Service Descriptions
6.2 Verification under Uncertainty
6.3 Special Cases
6.3.1 Loop Proof Obligations
6.3.2 Repetition
6.4 Discussion and Related Work
7 Prototypical Implementation
7.1 Overview
7.1.1 Automating Satisfiability Problems
7.1.2 Compatibility with SeSAME
7.1.3 Input Models
7.2 Logical Models
7.2.1 Logical Encoding Standard SMT-LIB
7.2.2 Encoding Proofs, Sets, and Polymorphic Types
7.3 Prototype Architecture
7.4 Evaluation
7.4.1 Approach
7.4.2 Results
7.4.3 Conclusion
III Discussion
8 Discussion and Conclusion
8.1 Related Approaches
8.2 Conclusion
8.3 Design Decisions
8.4 Future Work
IV Appendix
A Template Examples
A.1 Produce/Consume
A.2 Choose
A.3 Target Processing
A.4 Filter
B Listings
B.1 Counterexample
Bibliography
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.