close
1.

図書
図書
1. Formal methods for the design of real-time systems : International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004 : Revised lectures
Marco Bernardo, Flavio Corradini (eds.)
出版情報: Berlin : Springer, c2004  vi, 293 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3185
所蔵情報: loading…
目次情報: 続きを見る
Models and Languages / Part I：
Decision Problems for Timed Automata: A Survey / R. Alur ; P. Madhusudan
Timed Petri Nets: Efficiency of Asynchronous Systems / E. Bihler ; W. Vogler
Timed Process Algebra (With a Focus on Explicit Termination and Relative-Timing) / J.C.M. Baeten ; M.A. Reniers
Expressiveness of Timed Events and Timed Languages / D.R. Cacciagrano ; F. Corradini
Real Time and Stochastic Time / M. Bravetti
On the Semantic Foundations of Standard UML 2.0 / B.V. Selic
Tools and Applications / Part II：
A Tutorial on Uppaal / G. Behrmann ; A. David ; K.G. Larsen
The IF Toolset / M. Bozga ; S. Graf ; I. Ober ; J. Sifakis
Embedded Software Analysis with MOTOR / J.-P. Katoen ; H. Bohnenkamp ; R. Klaren ; H. Hermanns
Author Index
Models and Languages / Part I：
Decision Problems for Timed Automata: A Survey / R. Alur ; P. Madhusudan
Timed Petri Nets: Efficiency of Asynchronous Systems / E. Bihler ; W. Vogler
2.

図書
図書
2. Formal methods for mobile computing : 5th International School on Formal Methods for the Design of Computer, Communication, and Software Systems : SFM-Moby 2005, Bertinoro, Italy, April 26-30, 2005 : advanced lectures
Marco Bernardo, Alessandro Bogliolo (eds.)
出版情報: Berlin ; Tokyo : Springer, c2005  vi, 270 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3465
所蔵情報: loading…
3.

電子ブック
ＥＢ
3. Formal Methods for Mobile Computing
Communication, and Software Systems International School on Formal Methods for the Design of Computer, Marco Bernardo, Alessandro Bogliolo, Takeo Kanade
出版情報: Springer eBooks Computer Science , Springer Berlin / Heidelberg, 2005
所蔵情報: loading…
4.

電子ブック
ＥＢ
4. Formal Methods for Computational Systems Biology
Marco Bernardo, Pierpaolo Degano, Takeo Kanade, Gianluigi Zavattaro
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
目次情報: 続きを見る
Regular Lectures / Part I：
Sensitivity Analysis of Stochastic Models of Bistable Biochemical Reactions / Andrea Degasperi ; Stephen Gilmore
Pathway Logic / Carolyn Talcott
Formal Cell Biology in Biocham / Francois Fages ; Sylvain Soliman
Hierarchical Modeling for Computational Biology / Carsten Maus ; Mathias John ; Mathias Rohl ; Adelinde M. Uhrmacher
Simulation Methods in Systems Biology / Daniel T. Gillespie
Membrane Computing as a Modeling Framework. Cellular Systems Case Studies / Gheorghe Paun ; Francisco Jose Romero-Campero
Petri Nets for Systems and Synthetic Biology / Monika Heiner ; David Gilbert ; Robin Donaldson
Process Algebras in Systems Biology / Federica Ciocchetta ; Jane Hillston
The BlenX Language: A Tutorial / Lorenzo Dematte ; Corrado Priami ; Alessandro Romanel
BISCA Talks / Part II：
Cells in Silico: A Holistic Approach / Davide Chiarugi ; Pierpaolo Degano ; Jan Bert Van Klinken ; Roberto Marangoni
The Calculus of Looping Sequences / Roberto Barbuti ; Giulio Caravagna ; Andrea Maggiolo-Schettini ; Paolo Milazzo ; Giovanni Pardini
Hybrid Systems and Biology: Continuous and Discrete Modeling for Systems Biology / Luca Bortolussi ; Alberto Policriti
[pi]@: A [pi]-Based Process Calculus for the Implementation of Compartmentalised Bio-inspired Calculi / Cristian Versari ; Roberto Gorrieri
A Gentle Introduction to Stochastic (Poly)Automata Collectives and the (Bio)Chemical Ground Form / Gianluigi Zavattaro
Author Index
Regular Lectures / Part I：
Sensitivity Analysis of Stochastic Models of Bistable Biochemical Reactions / Andrea Degasperi ; Stephen Gilmore
Pathway Logic / Carolyn Talcott
5.

電子ブック
ＥＢ
5. Formal Methods for Hardware Verification
Marco Bernardo, Alessandro Cimatti, Takeo Kanade
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
6.

電子ブック
ＥＢ
6. Formal Methods for Web Services
Marco Bernardo, Takeo Kanade, Luca Padovani, Gianluigi Zavattaro
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2009
所蔵情報: loading…
目次情報: 続きを見る
Calculi for Service-Oriented Computing / Roberto Bruni
Service Interaction: Patterns, Formalization, and Analysis / Wil M.P. van der Aalst ; Arjan J. Mooij ; Christian Stahl ; Karsten Wolf
Synthesis and Composition of Web Services / Annapaola Marconi ; Marco Pistore
Fundamentals of Session Types / Vasco T. Vasconcelos
Asynchronous Session Types: Exceptions and Multiparty Interactions / Marco Carbone ; Nobuko Yoshida ; Kohei Honda
Contract-Based Discovery and Adaptation of Web Services / Luca Padovani
Contract-Based Discovery and Composition of Web Services / Mario Bravetti ; Gianluigi Zavattaro
Quantitative Analysis of Web Services Using SRMC / Allan Clark ; Stephen Gilmore ; Mirco Tribastone
Author Index
Calculi for Service-Oriented Computing / Roberto Bruni
Service Interaction: Patterns, Formalization, and Analysis / Wil M.P. van der Aalst ; Arjan J. Mooij ; Christian Stahl ; Karsten Wolf
Synthesis and Composition of Web Services / Annapaola Marconi ; Marco Pistore
7.

電子ブック
ＥＢ
7. Formal Methods for Quantitative Aspects of Programming Languages
Alessandro Aldini, Marco Bernardo, Takeo Kanade, Alessandra Pierro, Herbert Wiklicky
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
8.

電子ブック
ＥＢ
8. Computer Performance Engineering
Alessandro Aldini, Marco Bernardo, Luciano Bononi, Vittorio Cortellessa, Takeo Kanade
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
目次情報: 続きを見る
Invited Papers
Modeling and Experimenting with Vehicular Congestion for Distributed Advanced Traveler Information Systems / Marco Roccetti ; Gustavo Marfia
Application of Advanced Model-Driven Techniques in Performance Engineering / Lucia Kapova ; Ralf Reussner
Network and Software Performance
A New Markov-Based Mobility Prediction Algorithm for Mobile Networks / Samir Bellahsene ; Leila Kloul
Performance Aware Reconfiguration of Software Systems / Moreno Marzolla ; Raffaela Mirandola
On the Energy-Performance Tradeoff for Parallel Applications / Shikharesh Majumdar
Timed Models and Model Checking
A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking / Lasse Jacobsen ; Morten Jacobsen ; Mikael H. Møller ; Jirí Srba
Continuous Time and/or Continuous Distributions / Joseph Assouramou ; Josée Desharnais
Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report / Falko Dulat ; Joost-Pieter Katoen ; Viet Yen Nguyen
Case Studies
A Markovian Agent Model for Fire Propagation in Outdoor Environments / Davide Cerotti ; Marco Gribaudo ; Andrea Bobbio ; Carlos T. Calafate ; Pietro Manzoni
Queueing Network Models for Performance Evaluation of ZigBee-Based WSNs / Patrick Bellasi ; Adnan Faisal ; William Fornaciari ; Giuseppe Serazzi
Performance Modeling and Analysis of the Universal Control Hub / Elena Gómez-Martínez ; José Merseguer
Model Solutions and Bounds
Accurate Performance Estimation for Stochastic Marked Graphs by Bottleneck Regrowing / Ricardo J. Rodríguez ; Jorge Júlvez
A Numerical Algorithm for the Solution of Product-Form Models with Infinite State Spaces / Simonetta Balsamo ; Gian-Luca Dei Rossi ; Andrea Marin
State-Dependent Rates and Semi-Product-Form via the Reversed Process / Nigel Thomas ; Peter Harrison
Compositional Analysis
Predictive Modelling of Peer-to-Peer Event-Driven Communication in Component-Based Systems / Christoph Rathfelder ; David Evans ; Samuel Kounev
A Component-Based Solution Method for Non-ergodic Markov Regenerative Processes / Elvio Gilberto Amparore ; Susanna Donatelli
Compositional Abstraction of PEPA Models for Transient Analysis / Michael J.A. Smith
Composing Systems While Preserving Probabilities / Sonja Georgievska ; Suzana Andova
Author Index
Invited Papers
Modeling and Experimenting with Vehicular Congestion for Distributed Advanced Traveler Information Systems / Marco Roccetti ; Gustavo Marfia
Application of Advanced Model-Driven Techniques in Performance Engineering / Lucia Kapova ; Ralf Reussner
9.

電子ブック
ＥＢ
9. Formal Methods for Eternal Networked Software Systems
Marco Bernardo, Val?rie Issarny, Takeo Kanade
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2011
所蔵情報: loading…
10.

電子ブック
ＥＢ
10. A Process Algebraic Approach to Software Architecture Design
Alessandro Aldini, Marco Bernardo, Flavio Corradini
出版情報: Springer eBooks Computer Science , Springer London, 2010
所蔵情報: loading…
目次情報: 続きを見る
Process Calculi and Behavioral Equivalences / Part 1：
Process Algebra / 1：
Concurrency, Communication, and Nondeterminism / 1.1：
Running Example: Producer-Consumer System / 1.2：
PC: Process Calculus for Nondeterministic Processes / 1.3：
Syntax: Actions and Behavioral Operators / 1.3.1：
Semantics: Structural Operational Rules / 1.3.2：
Bisimulation Equivalence / 1.4：
Equivalence Relations and Preorders / 1.4.1：
Definition of the Behavioral Equivalence / 1.4.2：
Conditions and Characterizations / 1.4.3：
Congruence Property / 1.4.4：
Sound and Complete Axiomatization / 1.4.5：
Modal Logic Characterization / 1.4.6：
Verification Algorithm / 1.4.7：
Abstracting from Invisible Actions / 1.4.8：
Testing Equivalence / 1.5：
Trace Equivalence / 1.5.1：
The Linear-Time/Branching-Time Spectrum / 1.6.1：
Deterministically Timed Process Algebra / 2：
Concurrency, Communication, and Deterministic Time / 2.1：
Deterministically Timed Process Calculi / 2.2：
TPC: Timed Process Calculus with Durationless Actions / 2.2.1：
DPC: Timed Process Calculus with Durational Actions / 2.2.2：
Deterministically Timed Behavioral Equivalences / 2.3：
Definition of Timed Bisimulation Equivalence / 2.3.1：
Durational Bisimulation Equivalence and its Properties / 2.3.2：
Semantics-Preserving Mapping for Eagerness / 2.4：
Differences Between TPC and DPC / 2.4.1：
From DPC to TPC Under Eagerness / 2.4.2：
Semantics-Preserving Mapping for Laziness / 2.5：
Lazy TPC / 2.5.1：
Lazy DPC / 2.5.2：
From DPC to TPC Under Laziness / 2.5.3：
Semantics-Preserving Mapping for Maximal Progress / 2.6：
Maximal Progress TPC / 2.6.1：
Maximal Progress DPC / 2.6.2：
From DPC to TPC Under Maximal Progress / 2.6.3：
Expressiveness of Eagerness, Laziness, Maximal Progress / 2.7：
Synchronization Issues / 2.7.1：
Choosing at Different Times / 2.7.2：
Performing Infinitely Many Actions at the Same Time / 2.7.3：
Performing Finitely Many Actions at the Same Time / 2.7.4：
Coincidence Result for Sequential Processes / 2.7.5：
Stochastically Timed Process Algebra / 3：
Concurrency, Communication, and Stochastic Time / 3.1：
MPC: Markovian Process Calculus with Durational Actions / 3.2：
Markov Chains / 3.2.1：
Syntax and Semantics / 3.2.2：
Markovian Bisimulation Equivalence / 3.3：
Exit Rates and Exit Probabilities / 3.3.1：
Abstracting from Invisible Actions with Zero Duration / 3.3.2：
Markovian Testing Equivalence / 3.4：
Probability and Duration of Computations / 3.4.1：
Markovian Trace Equivalence / 3.4.2：
Exactness of Markovian Behavioral Equivalences / 3.5.1：
The Markovian Linear-Time/Branching-Time Spectrum / 3.7：
Process Algebra for Software Architecture / Part II：
Component-Oriented Modeling / 4：
Software Architecture Description Languages / 4.1：
Running Example: Client-Server System / 4.2：
Architectural Upgrade of Process Algebra: Guidelines / 4.3：
G1: Separating Behavior and Topology Descriptions / 4.3.1：
G2: Reusing Component and Connector Specification / 4.3.2：
G3: Eliciting Component and Connector Interface / 4.3.3：
G4: Classifying Communication Synchronicity / 4.3.4：
G5: Classifying Communication Multiplicity / 4.3.5：
G6: Textual and Graphical Notations (PADL Syntax) / 4.3.6：
G7: Dynamic and Static Operators / 4.3.7：
Translation Semantics for PADL / 4.4：
Semantics of Individual Elements / 4.4.1：
Semantics of Interacting Elements / 4.4.2：
Summarizing Example: Pipe-Filter System / 4.5：
G8: Supporting Architectural Styles / 4.6：
Architectural Types / 4.6.1：
Hierarchical Modeling / 4.6.2：
Behavioral Conformity / 4.6.3：
Exogenous Variations / 4.6.4：
Endogenous Variations / 4.6.5：
Multiplicity Variations / 4.6.6：
Comparisons / 4.7：
Comparison with Process Algebra / 4.7.1：
Comparison with Parallel Composition Operators / 4.7.2：
Comparison with Other Software Architecture Languages / 4.7.3：
Component-Oriented Functional Verification / 5：
Mismdet: Architecture-Level Mismatch Detection / 5.1：
Class of Properties and Detection Strategy / 5.2：
Architectural Compatibility of Star-Shaped Topologies / 5.3：
Case Study: Compressing Proxy System / 5.3.1：
Architectural Interoperability of Cycle-Shaped Topologies / 5.4：
Case Study: Cruise Control System / 5.4.1：
Generalization to Arbitrary Topologies / 5.5：
Case Study: Simulator for the Cruise Control System / 5.5.1：
Generalization to Architectural Types / 5.6：
Generalization to Internal Behavioral Variations / 5.6.1：
Generalization to Exogenous Variations / 5.6.2：
Generalization to Endogenous Variations / 5.6.3：
Generalization to Multiplicity Variations / 5.6.4：
Component-Oriented Performance Evaluation / 5.7：
Perfsel: Performance-Driven Architectural Selection / 6.1：
Class of Measures and Selection Strategy / 6.2：
Emilia: Extending PADL with Performance Aspects / 6.3：
Queueing Systems and Queueing Networks / 6.4：
From ÆEmilia Descriptions to Queueing Networks / 6.5：
General Syntactical Restrictions / 6.5.1：
Queueing Network Basic Elements / 6.5.2：
Documental Functions / 6.5.3：
Characterizing Functions / 6.5.4：
Case Study: Selecting Compiler Architectures / 6.6：
Sequential Architecture / 6.6.1：
Pipeline Architecture / 6.6.2：
Concurrent Architecture / 6.6.3：
Scenario-Based Performance Selection / 6.6.4：
Trading Dependability and Performance / 6.7：
DepPerf: Mixed View of Dependability and Performance / 7.1：
Running Example: Multilevel Security Routing System / 7.2：
First Phase of DepPerf: Noninterference Analysis / 7.3：
Noninterference Theory / 7.3.1：
Noninterference Verification / 7.3.2：
Component-Oriented Noninterference Check / 7.3.3：
Interpretation and Feedback / 7.3.4：
Second Phase of DepPerf: Performance Evaluation / 7.4：
Model Validation / 7.4.1：
Analysis and Tuning / 7.4.2：
Measure Specification Language / 7.4.3：
Case Study I: The Network NRL Pump / 7.5：
Informal Specification / 7.5.1：
Architectural Description / 7.5.2：
Noninterference Analysis / 7.5.3：
Performance Evaluation / 7.5.4：
Case Study II: Power-Manageable System / 7.6：
References / 7.6.1：
Index
Process Calculi and Behavioral Equivalences / Part 1：
Process Algebra / 1：
Concurrency, Communication, and Nondeterminism / 1.1：
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼