close
1.

電子ブック

EB
Frank S. Boer, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Takeo Kanade, Willem-Paul Roever
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Component and Service Oriented Computing
A Software Component Model and Its Preliminary Formalisation / Kung-Kiu Lau ; Mario Ornaghi ; Zheng Wang
Synchronised Hyperedge Replacement as a Model for Service Oriented Computing / Gian Luigi Ferrari ; Dan Hirsch ; Ivan Lanese ; Ugo Montanari ; Emilio Tuosto
System Design
Control of Modular and Distributed Discrete-Event Systems / Jan Komenda ; Jan H. van Schuppen
Model-Based Security Engineering with UML: Introducing Security Aspects / Jan Jurjens
The Pragmatics of Stairs / Ragnhild Kobro Runde ; Oystein Haugen ; Ketil Stolen
Tools
Smallfoot: Modular Automatic Assertion Checking with Separation Logic / Josh Berdine ; Cristiano Calcagno ; Peter W. O'Hearn
Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs / Dennis R. Dams ; Kedar S. Namjoshi
Algebraic Methods
Beyond Bisimulation: The "up-to" Techniques / Davide Sangiorgi
Separation Results Via Leader Election Problems / Maria Grazia Vigliotti ; Iain Phillips ; Catuscia Palamidessi
Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation / Wan Fokkink ; Rob van Glabbeek ; Paulien de Wind
Model Checking
Abstraction and Refinement in Model Checking / Orna Grumberg
Program Compatibility Approaches / Edmund Clarke ; Natasha Sharygina ; Nishant Sinha
Cluster-Based LTL Model Checking of Large Systems / Jiri Barnat ; Lubos Brim ; Ivana Cerna
Safety and Liveness in Concurrent Pointer Programs / Dino Distefano ; Joost-Pieter Katoen ; Arend Rensink
Assertional Methods
Modular Specification of Encapsulated Object-Oriented Components / Arnd Poetzsch-Heffter ; Jan Schafer
Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 / Patrice Chalin ; Joseph R. Kiniry ; Gary T. Leavens ; Erik Poll
Boogie: A Modular Reusable Verifier for Object-Oriented Programs / Mike Barnett ; Bor- Yuh Evan Chang ; Robert DeLine ; Bart Jacobs ; K. Rustan M. Leino
Quantitative Analysis
On a Probabilistic Chemical Abstract Machine and the Expressiveness of Linda Languages / Alessandra Di Pierro ; Chris Hankin ; Herbert Wiklicky
Partial Order Reduction for Markov Decision Processes: A Survey / Marcus Groesser ; Christel Baier
Author Index
Component and Service Oriented Computing
A Software Component Model and Its Preliminary Formalisation / Kung-Kiu Lau ; Mario Ornaghi ; Zheng Wang
Synchronised Hyperedge Replacement as a Model for Service Oriented Computing / Gian Luigi Ferrari ; Dan Hirsch ; Ivan Lanese ; Ugo Montanari ; Emilio Tuosto
2.

電子ブック

EB
Frank S. Boer, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Takeo Kanade, Willem-Paul Roever
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
3.

電子ブック

EB
Gilles Barthe, Frank S. Boer, Frank S. de Boer, Takeo Kanade, IFIP Working Group 6.1.
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
4.

電子ブック

EB
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
5.

電子ブック

EB
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
6.

電子ブック

EB
Frank S. Boer, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Takeo Kanade, Willem-Paul Roever
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2007
所蔵情報: loading…
目次情報: 続きを見る
Testing
Model-Based Testing of Environmental Conformance of Components / Lars Frantzen ; Jan Tretmans
Exhaustive Testing of Exception Handlers with Enforcer / Cyrille Artho ; Armin Biere ; Shinichi Honiden
Model-Based Test Selection for Infinite-State Reactive Systems / Bertrand Jeannet ; Thierry Jeron ; Vlad Rusu
Program Verification
Verifying Object-Oriented Programs with KeY: A Tutorial / Wolfgang Ahrendt ; Bernhard Beckert ; Reiner Hahnle ; Philipp Rummer ; Peter H. Schmitt
Rebeca: Theory, Applications, and Tools / Marjan Sirjani
Learning Meets Verification / Martin Leucker
Trust and Security
JACK-A Tool for Validation of Security and Behaviour of Java Applications / Gilles Barthe ; Lilian Burdy ; Julien Charles ; Benjamin Gregoire ; Marieke Huisman ; Jean-Louis Lanet ; Mariela Pavlova ; Antoine Requet
Towards a Formal Framework for Computational Trust / Vladimiro Sassone ; Karl Krukow ; Mogens Nielsen
Models of Computation
On Recursion, Replication and Scope Mechanisms in Process Calculi / Jesus Aranda ; Cinzia Di Giusto ; Catuscia Palamidessi ; Frank D. Valencia
Bounded Session Types for Object Oriented Languages / Mariangiola Dezani-Ciancaglini ; Elena Giachino ; Sophia Drossopoulou ; Nobuko Yoshida
Distributed Programming
Reflecting on Aspect-Oriented Programming, Metaprogramming, and Adaptive Distributed Monitoring / Bill Donkervoet ; Gul Agha
Links: Web Programming Without Tiers / Ezra Cooper ; Sam Lindley ; Philip Wadler ; Jeremy Yallop
Author Index
Testing
Model-Based Testing of Environmental Conformance of Components / Lars Frantzen ; Jan Tretmans
Exhaustive Testing of Exception Handlers with Enforcer / Cyrille Artho ; Armin Biere ; Shinichi Honiden
7.

電子ブック

EB
Frank S. Boer, Marcello M. Bonsangue, Stefan Hallerstede, Takeo Kanade, Michael Leuschel
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
目次情報: 続きを見る
The BIONETS Project
A Framework for Reasoning on Component Composition / Ludovic Henrio ; Florian Kammüller ; Muhammad Uzair Khan
The COMPAS Project
Verification of Context-Dependent Channel-Based Service Models / Natallia Kokash ; Christian Krause ; Erik P. de Vink
The CREDO Project
The Credo Methodology (Extended Version) / Immo Grabe ; Mohammad Mahdi Jaghoori ; Joachim Klein ; Sascha Klüppelholz ; Andries Stam ; Christel Baier ; Tobias Blechmann ; Bernhard K. Aichernig ; Frank de Boer ; Andreas Griesmayer ; Einar Broch Johnsen ; Marcel Kyas ; Wolfgang Leister ; Rudolf Schlatte ; Martin Steffen ; Simon Tschirner ; Liang Xuedong ; Wang Yi
The DEPLOY Project
Guided Formal Development: Patterns for Modelling and Refinement / Alexei Iliasov ; Elena Troubitsyna ; Linas Laibinis ; Alexander Romanovsky
Applying Event-B Atomicity Decomposition to a Multi Media Protocol / Asieh Salehi Fathabadi ; Michael Butler
The FM-SOA Working Group
Abstract Certification of Global Non-interference in Rewriting Logic / Mauricio Alba-Castro ; María Alpuente ; Santiago Escobar
The HATS Project
Interleaving Symbolic Execution and Partial Evaluation / Richard Bubel ; Reiner Hähnle ; Ran Ji
The INESS Project
The Use of Model Transformation in the INESS Project / Osmar M. dos Santos ; Jim Woodcock ; Richard F. Paige ; Steve King
Suitability of mCRL2 for Concurrent-System Design: A 2 x 2 Switch Case Study / Frank P.M. Stappers ; Michel A. Reniers ; Jan Friso Groote
The MOGENTES Project
Mapping UML to Labeled Transition Systems for Test-Case Generation: A Translation via Object-Oriented Action Systems / Willibald Krenn ; Rupert Schlick
Mutation-Based Test Case Generation for Simulink Models / Angelo Brillout ; Nannan He ; Michele Mazzucchi ; Daniel Kroening ; Mitra Purandare ; Philipp Rümmer ; Georg Weissenbacher
Model-Based Mutation Testing of Hybrid Systems / Harald Brandl ; Elisabeth Jöbstl
The PROTEST Project
Property-Based Testing - The ProTest Project / John Derrick ; Neil Walkinshaw ; Thomas Arts ; Clara Benac Earle ; Francesco Cesarini ; Lars-Ake Fredlund ; Victor Gulias ; John Hughes ; Simon Thompson
Incrementally Discovering Testable Specifications from Program Executions
The QUASIMODO Project
Methodologies for Specification of Real-Time Systems Using Timed I/O Automata / Alexandre David ; Kim G. Larsen ; Axel Legay ; Ulrik Nyman ; Andrzej Wasowski
The How and Why of Interactive Markov Chains / Holger Hermanns ; Joost-Pieter Katoen
Author Index
The BIONETS Project
A Framework for Reasoning on Component Composition / Ludovic Henrio ; Florian Kammüller ; Muhammad Uzair Khan
The COMPAS Project
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼