close
1.

電子ブック
ＥＢ
1. Formal Methods for Components and Objects
Frank S. Boer, Marcello M. Bonsangue, Takeo Kanade, Eric Madelaine
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2009
所蔵情報: loading…
目次情報: 続きを見る
The COMPAS Project
Reusable Architectural Decision Model for Model and Metadata Repositories / Christine Mayr ; Uwe Zdun ; Schahram Dustdar
Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems / Natallia Kokash ; Farhad Arbab
The CREDO Project
A Real-Time Extension of Creol for Modelling Biomedical Sensors / Marcel Kyas ; Einar Broch Johnsen
Conformance Testing of Distributed Concurrent Systems with Executable Designs / Bernhard K. Aichernig ; Andreas Griesmayer ; Rudolf Schlatte ; Andries Stam
Formal Verification for Components and Connectors / Christel Baier ; Tobias Blechmann ; Joachim Klein ; Sascha Kt&uuuml;ppelholz
The DEPLOY Project
Formal Modular Modelling of Context-Awareness / Mats Neovius ; Kaisa Sere
Towards Demonstrably Correct Compilation of Java Byte Code / Michael Leuschel
Incremental System Modelling in Event-B / Stefan Hallerstede
The GRIDCOMP Project
An Asynchronous Distributed Component Model and Its Semantics / Ludovic Henrio ; Florian Kamm&uuuml;ller ; Marcela Rivera
Specification and Verification for Grid Component-Based Applications: From Models to Tools / Antonio Cansado ; Eric Madelaine
Semi-formal Models to Support Program Development: Autonomic Management within Component Based Parallel and Distributed programming / M. Aldinucci ; M. Danelutto ; P. Kilpatrick
The MOBIUS Project
Session-Based Compilation Framework for Multicore Programming / Nobuko Yoshida ; Vasco Vasconcelos ; Hervé Paulino ; Kohei Honda
Abstract Interpretation of Symbolic Execution with Explicit State Updates / Richard Bubel ; Reiner Hähnle ; Benjamin Weiß
BML and Related Tools / Jacek Chrz&acedil;szcz ; Marieke Huisman ; Aleksy Schubert
Author Index
The COMPAS Project
Reusable Architectural Decision Model for Model and Metadata Repositories / Christine Mayr ; Uwe Zdun ; Schahram Dustdar
Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems / Natallia Kokash ; Farhad Arbab
2.

電子ブック
ＥＢ
2. Verification of Sequential and Concurrent Programs
Krzysztof R. Apt, Frank S. Boer, Ernst-R?diger Olderog
出版情報: Springer eBooks Computer Science , Springer London, 2009
所蔵情報: loading…
目次情報: 続きを見る
Endorsements
Foreword
Preface
Outlines of One-semester Courses
In the Beginning / Part I：
Introduction / 1：
An Example of a Concurrent Program / 1.1：
Solution 1
Solution 2
Solution 3
Solution 4
Solution 5
Solution 6
Program Correctness / 1.2：
Structure of this Book / 1.3：
Automating Program Verification / 1.4：
Assertional Methods in Practice / 1.5：
Preliminaries / 2：
Mathematical Notation / 2.1：
Sets
Tuples
Relations
Functions
Sequences
Strings
Proofs
Induction
Grammars
Typed Expressions / 2.2：
Types
Variables
Constants
Expressions
Subscripted Variables
Semantics of Expressions / 2.3：
Fixed Structure
States
Definition of the Semantics
Updates of States
Formal Proof Systems / 2.4：
Assertions / 2.5：
Semantics of Assertions / 2.6：
Substitution / 2.7：
Substitution Lemma / 2.8：
Exercises / 2.9：
Bibliographic Remarks / 2.10：
Deterministic Programs / Part II：
while Programs / 3：
Syntax / 3.1：
Semantics / 3.2：
Properties of Semantics
Verification / 3.3：
Partial Correctness
Total Correctness
Decomposition
Soundness
Proof Outlines / 3.4：
Completeness / 3.5：
Parallel Assignment / 3.6：
Failure Statement / 3.7：
Auxiliary Axioms and Rules / 3.8：
Case Study: Partitioning an Array / 3.9：
Systematic Development of Correct Programs / 3.10：
Summation Problem
Case Study: Minimum-Sum Section Problem / 3.11：
Recursive Programs / 3.12：
Properties of the Semantics / 4.1：
Discussion / 4.3：
Case Study: Binary Search / 4.4：
Recursive Programs with Parameters / 4.5：
Partial Correctness: Non-recursive Procedures / 5.1：
Partial Correctness: Recursive Procedures
Modularity
Case Study: Quicksort / 5.4：
Formal Problem Specification
Properties of Partition
Auxiliary Proof: Permutation Property
Auxiliary Proof: Sorting Property
Object-Oriented Programs / 5.5：
Local Expressions / 6.1：
Statements and Programs
Semantics of Local Expressions / 6.2：
Semantics of Statements and Programs
Adding Parameters / 6.3：
Transformation of Object-Oriented Programs / 6.6：
Object Creation / 6.7：
Case Study: Zero Search in Linked List / 6.8：
Case Study: Insertion into a Linked List / 6.9：
Parallel Programs / 6.10：
Disjoint Parallel Programs / 7：
Determinism / 7.1：
Sequentialization
Parallel Composition / 7.3：
Auxiliary Variables
Case Study: Find Positive Element / 7.4：
Parallel Programs with Shared Variables / 7.5：
Access to Shared Variables / 8.1：
Atomicity / 8.2：
Verification: Partial Correctness / 8.4：
Component Programs
No Compositionality of Input/Output Behavior
Parallel Composition: Interference Freedom
Auxiliary Variables Needed
Verification: Total Correctness / 8.5：
Case Study: Find Positive Element More Quickly / 8.6：
Allowing More Points of Interference / 8.7：
Case Study: Parallel Zero Search / 8.8：
Simplifying the program / Step 1：
Proving partial correctness / Step 2：
Parallel Programs with Synchronization / 8.9：
Weak Total Correctness / 9.1：
Case Study: Producer/Consumer Problem / 9.4：
Case Study: The Mutual Exclusion Problem / 9.5：
Problem Formulation
A Busy Wait Solution
A Solution Using Semaphores
Case Study: Synchronized Zero Search / 9.6：
Simplifying the Program
Decomposing Total Correctness
Proving Termination / Step 3：
Proving Partial Correctness / Step 4：
Nondeterministic and Distributed Programs / 9.8：
Nondeterministic Programs / 10：
Why Are Nondeterministic Programs Useful? / 10.1：
Symmetry
Nondeterminism
Failures
Modeling Concurrency
Case Study: The Welfare Crook Problem / 10.4：
Transformation of Parallel Programs / 10.6：
Distributed Programs / 10.7：
Sequential Processes / 11.1：
Transformation into Nondeterministic Programs / 11.2：
Semantic Relationship Between S and T(S)
Proof of the Sequentialization Theorem
Proof Systems / 11.4：
Case Study: A Transmission Problem / 11.5：
Proving Absence of Failures and of Divergence
Proving Deadlock Freedom
Fairness / 11.6：
The Concept of Fairness / 12.1：
Selections and Runs
Fair Nondeterminism Semantics
Transformational Semantics / 12.2：
Well-Founded Structures / 12.3：
Random Assignment / 12.4：
Schedulers / 12.5：
The Scheduler FAIR
The Scheduler RORO
The Scheduler QUEUE
Transformation / 12.6：
Case Study: Zero Search / 12.7：
Case Study: Asynchronous Fixed Point Computation / 12.9：
Axioms and Proof Rules / 12.10：
References / C：
Index
Author Index
Symbol Index
Endorsements
Foreword
Preface
3.

電子ブック
ＥＢ
3. Formal Methods for Components and Objects
Frank S. Boer, Marcello M. Bonsangue, Takeo Kanade, Eric Madelaine, Josef Kittler
出版情報: SpringerLink Books - AutoHoldings , Springer Berlin Heidelberg, 2009
所蔵情報: loading…
目次情報: 続きを見る
The COMPAS Project
Reusable Architectural Decision Model for Model and Metadata Repositories / Christine Mayr ; Uwe Zdun ; Schahram Dustdar
Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems / Natallia Kokash ; Farhad Arbab
The CREDO Project
A Real-Time Extension of Creol for Modelling Biomedical Sensors / Marcel Kyas ; Einar Broch Johnsen
Conformance Testing of Distributed Concurrent Systems with Executable Designs / Bernhard K. Aichernig ; Andreas Griesmayer ; Rudolf Schlatte ; Andries Stam
Formal Verification for Components and Connectors / Christel Baier ; Tobias Blechmann ; Joachim Klein ; Sascha Kt&uuuml;ppelholz
The DEPLOY Project
Formal Modular Modelling of Context-Awareness / Mats Neovius ; Kaisa Sere
Towards Demonstrably Correct Compilation of Java Byte Code / Michael Leuschel
Incremental System Modelling in Event-B / Stefan Hallerstede
The GRIDCOMP Project
An Asynchronous Distributed Component Model and Its Semantics / Ludovic Henrio ; Florian Kamm&uuuml;ller ; Marcela Rivera
Specification and Verification for Grid Component-Based Applications: From Models to Tools / Antonio Cansado ; Eric Madelaine
Semi-formal Models to Support Program Development: Autonomic Management within Component Based Parallel and Distributed programming / M. Aldinucci ; M. Danelutto ; P. Kilpatrick
The MOBIUS Project
Session-Based Compilation Framework for Multicore Programming / Nobuko Yoshida ; Vasco Vasconcelos ; Hervé Paulino ; Kohei Honda
Abstract Interpretation of Symbolic Execution with Explicit State Updates / Richard Bubel ; Reiner Hähnle ; Benjamin Weiß
BML and Related Tools / Jacek Chrz&acedil;szcz ; Marieke Huisman ; Aleksy Schubert
Author Index
The COMPAS Project
Reusable Architectural Decision Model for Model and Metadata Repositories / Christine Mayr ; Uwe Zdun ; Schahram Dustdar
Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems / Natallia Kokash ; Farhad Arbab
4.

電子ブック
ＥＢ
4. Verification of Sequential and Concurrent Programs
Krzysztof R. Apt, Frank S. Boer, Ernst-Rüdiger Olderog
出版情報: SpringerLink Books - AutoHoldings , Springer London, 2009
所蔵情報: loading…
目次情報: 続きを見る
Endorsements
Foreword
Preface
Outlines of One-semester Courses
In the Beginning / Part I：
Introduction / 1：
An Example of a Concurrent Program / 1.1：
Solution 1
Solution 2
Solution 3
Solution 4
Solution 5
Solution 6
Program Correctness / 1.2：
Structure of this Book / 1.3：
Automating Program Verification / 1.4：
Assertional Methods in Practice / 1.5：
Preliminaries / 2：
Mathematical Notation / 2.1：
Sets
Tuples
Relations
Functions
Sequences
Strings
Proofs
Induction
Grammars
Typed Expressions / 2.2：
Types
Variables
Constants
Expressions
Subscripted Variables
Semantics of Expressions / 2.3：
Fixed Structure
States
Definition of the Semantics
Updates of States
Formal Proof Systems / 2.4：
Assertions / 2.5：
Semantics of Assertions / 2.6：
Substitution / 2.7：
Substitution Lemma / 2.8：
Exercises / 2.9：
Bibliographic Remarks / 2.10：
Deterministic Programs / Part II：
while Programs / 3：
Syntax / 3.1：
Semantics / 3.2：
Properties of Semantics
Verification / 3.3：
Partial Correctness
Total Correctness
Decomposition
Soundness
Proof Outlines / 3.4：
Completeness / 3.5：
Parallel Assignment / 3.6：
Failure Statement / 3.7：
Auxiliary Axioms and Rules / 3.8：
Case Study: Partitioning an Array / 3.9：
Systematic Development of Correct Programs / 3.10：
Summation Problem
Case Study: Minimum-Sum Section Problem / 3.11：
Recursive Programs / 3.12：
Properties of the Semantics / 4.1：
Discussion / 4.3：
Case Study: Binary Search / 4.4：
Recursive Programs with Parameters / 4.5：
Partial Correctness: Non-recursive Procedures / 5.1：
Partial Correctness: Recursive Procedures
Modularity
Case Study: Quicksort / 5.4：
Formal Problem Specification
Properties of Partition
Auxiliary Proof: Permutation Property
Auxiliary Proof: Sorting Property
Object-Oriented Programs / 5.5：
Local Expressions / 6.1：
Statements and Programs
Semantics of Local Expressions / 6.2：
Semantics of Statements and Programs
Adding Parameters / 6.3：
Transformation of Object-Oriented Programs / 6.6：
Object Creation / 6.7：
Case Study: Zero Search in Linked List / 6.8：
Case Study: Insertion into a Linked List / 6.9：
Parallel Programs / 6.10：
Disjoint Parallel Programs / 7：
Determinism / 7.1：
Sequentialization
Parallel Composition / 7.3：
Auxiliary Variables
Case Study: Find Positive Element / 7.4：
Parallel Programs with Shared Variables / 7.5：
Access to Shared Variables / 8.1：
Atomicity / 8.2：
Verification: Partial Correctness / 8.4：
Component Programs
No Compositionality of Input/Output Behavior
Parallel Composition: Interference Freedom
Auxiliary Variables Needed
Verification: Total Correctness / 8.5：
Case Study: Find Positive Element More Quickly / 8.6：
Allowing More Points of Interference / 8.7：
Case Study: Parallel Zero Search / 8.8：
Simplifying the program / Step 1：
Proving partial correctness / Step 2：
Parallel Programs with Synchronization / 8.9：
Weak Total Correctness / 9.1：
Case Study: Producer/Consumer Problem / 9.4：
Case Study: The Mutual Exclusion Problem / 9.5：
Problem Formulation
A Busy Wait Solution
A Solution Using Semaphores
Case Study: Synchronized Zero Search / 9.6：
Simplifying the Program
Decomposing Total Correctness
Proving Termination / Step 3：
Proving Partial Correctness / Step 4：
Nondeterministic and Distributed Programs / 9.8：
Nondeterministic Programs / 10：
Why Are Nondeterministic Programs Useful? / 10.1：
Symmetry
Nondeterminism
Failures
Modeling Concurrency
Case Study: The Welfare Crook Problem / 10.4：
Transformation of Parallel Programs / 10.6：
Distributed Programs / 10.7：
Sequential Processes / 11.1：
Transformation into Nondeterministic Programs / 11.2：
Semantic Relationship Between S and T(S)
Proof of the Sequentialization Theorem
Proof Systems / 11.4：
Case Study: A Transmission Problem / 11.5：
Proving Absence of Failures and of Divergence
Proving Deadlock Freedom
Fairness / 11.6：
The Concept of Fairness / 12.1：
Selections and Runs
Fair Nondeterminism Semantics
Transformational Semantics / 12.2：
Well-Founded Structures / 12.3：
Random Assignment / 12.4：
Schedulers / 12.5：
The Scheduler FAIR
The Scheduler RORO
The Scheduler QUEUE
Transformation / 12.6：
Case Study: Zero Search / 12.7：
Case Study: Asynchronous Fixed Point Computation / 12.9：
Axioms and Proof Rules / 12.10：
References / C：
Index
Author Index
Symbol Index
Endorsements
Foreword
Preface
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼