Formal Methods && Tools Group

2015 events

FMSPLE 2015: 6th International Workshop on Formal Methods and Analysis in Software Product Line Engineering, 11 April 2015, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, 11-18 April 2015

2014 events

FASE 2014: 17th International Conference on Fundamental Approaches to Software Engineering, Grenoble, France, 5-13 April 2014

FM 2014: 19th International Symposium on Formal Methods, Singapore, 14-16 May 2014

FMSPLE 2014: 5th International Workshop on Formal Methods and Analysis in Software Product Line Engineering, 10 October 2014, held as track of the 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Corfu, Greece, 8-11 October 2014

FormaliSE 2014: 2nd FME workshop on formal methods in software engineering, Hyderabad, India, 3 June 2014

SPLC 2014: 18th International Software Product Line Conference, Florence, Italy, 15-19 September 2014

VaMoS 2014: 8th International Workshop on Variability Modelling of Software-intensive Systems, Nice, France, January 22-24

WWV 2014: 10th International Workshop on Automated Specification and Verification of Web Systems, Vienna, Austria, 18 July 2014

2013 events

VAMOS 2013: 7th International Workshop on Variability Modelling of Software-intensive Systems, Pisa, Italy, 23-25 January 2013

FormaliSE 2013: 1st FME workshop on formal methods in software engineering, San Francisco, CA, USA, 18-26 May 2014

SPLC 2013: 17th International Software Product Line Conference, Tokio, Japan, 26-30 August 2013

2012 events

iFM & ABZ 2012 Joint conference in honour of Egon Boerger’s 65th birthday for his contribution to state-based formal methods, ISTI-CNR, Pisa, Italy, 18-22 June 2012

QAPL 2012, 10th Workshop on Quantitative Aspects of Programming Languages, Tallinn, Estonia, March 31 - April 1, 2012. Satellite WS of ETAPS2012.

VaMoS 2012 Sixth International Workshop on Variability Modelling of Software-intensive Systems, Leipzig, Germany, 25-27 January, 2012

FM 2012 18th International Symposium on Formal Methods, CNAM Paris France August 27-31 2012

SPLC 2012 16th International Software Product Line Conference, Costa da Sauipe September 02-07 2012

FormSERA Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA) Workshop on Saturday 2 June 2012, Zurich, Switzerland, in conjunction with ICSE 2012

WS-FM 2012: 9th International Workshop on Web Services and Formal Methods, Tallinn, Estonia, 6-7 September 2012

FMSPLE 2012: 3rd International Workshop on Formal Methods and Analysis in Software Product Line Engineering, Salvador, Brazil, 2 September 2012

2010-2011 events

QAPL 2011, 9th Workshop on Quantitative Aspects of Programming Languages, Saarbruecken, Germany, April 1-3, 2011. Satellite WS of ETAPS2011.
SEFM 2010 8th IEEE International Conference on Software Engineering and Formal Methods, ISTI CNR (Pisa) September 13-18 2010
ISARCS 2010: 1st International Symposium on Architecting Critical Systems Federated with CompArch 2010 Prague Czech Republic June 23-25 2010
WS-FM 2010 7th International Workshop on Web Services and Formal Methods, Stevens Institute of Technology Hoboken New Jersey USA September 16-17 2010
FMICS 2010 15th International Workshop on Formal Methods for Industrial Critical Systems, Antwerp Belgium September 20-21, 2010
ISoLA2010 4th International Symposium On Leveraging Applications of Formal Methods Verification and Validation, Amirandes Heraclion Crete October 18-20 2010
IFM 2010 8th International Conference, Nancy France October 11 - 14 2010
ICFEM 2010 12th International Conference on Formal Engineering Methods, Shanghai, China 16-19 November 2010.
ICSE 2010 32nd International Conference on Software Engineering
Vamos 2010 Fourth International Workshop on Variability Modelling of Software-intensive Systems

Past events

Vamos 2009
ICFEM 09FM+AM'09
SEFM 09
OPENCERT 2009
FM 2009
SPLC 2009
Fmics 2009
YR-SOC 2009
SPLC 08SEFM 08
SofSem 2008
ICFEM 2008
Fmics 2008
Serene 2008
STM 2008
Isola 2008
China 2008
VODCA 2008
FM'08
ESOP 07
FMICS 07
DASD 07
ASSE 2007
SPLC 07
REFSQ 06
EFTS 2006
SPLC 2006
FM 06
BPM 2006
VODCA 2006
FMICS 05
FORTE 2005
SEFM 2005
ICEIS 2005
FM 2005
ICSE 2005

VODCA 2004
ICFEM 2004
ATVA 2004
FMICS 2004
WS-FM04
DASD 2004
SEFM 2004
FORTE 2004
PFE-5 2003
ICEIS 2003
SEFM 2003
FMICS 2003
FORTE 2003
FM 2003
FORTE 2002
FM&&T Day
ISODARCO 2002
From the Distributed Systems to Internet: A day held in Norma Lijtmaer's honour
FMICS 2002
I3 Spring Days 2001
FORTE 2001
FMICS 01
FMICS 00
IFIP EUROCONFERENCE
FORTE 2000
CHI 2000
Elsewhere 2000
FMICS 99
ISODARCO 99
SPIN Workshop 99
FORTE 99
FMICS 98
FMICS 97
FMICS 96

Seminars


2013 Seminars

28 May 2013
Speaker: Laura Nenzi (IMT Lucca)
Title: A temporal logic approach to modular design of synthetic biological circuits

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a new approach for the design of a synthetic biological circuit whose behavior is specified in terms of signal temporal logic (STL) formulae. We first show how to characterize with STL formulae the input/output behavior of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behavior of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesizing a biological implementation of an half-adder.
Slides

28 May 2013
Speaker: Roberta Lanziani (IMT Lucca)
Title: Central Limit Approximation for Stochastic Model Checking

Abstract ⇲

Abstract ⇱

Abstract ⇱

In this talk we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.
Slides

28 May 2013
Speaker: Roberta Lanziani (IMT Lucca)
Title: Central Limit Approximation for Stochastic Model Checking

Abstract ⇲

Abstract ⇱

Abstract ⇱

In this talk we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.
Slides

27 May 2013
Speaker: Alessio Ferrari (ISTI CNR)
Title: Using collective intelligence to detect natural language pragmatic ambiguities

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding “concept paths” within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the presentation to illustrate the soundness of the proposed strategy.
NOTE: This seminar is the fourth one of the series of six seminars presented by the winners of the prize “Young researchers ISTI 2013”. Alessio Ferrari placed first in the Young researcher category.
Slides

22 May 2013
Speaker: Simon Davies ( LSE Enterprise, a wholly owned subsidiary of The London School of Economics and Political Science, London, UK)
Title: Europe's new data protection framework and what it means to IT engineering

Abstract ⇲

Abstract ⇱

Abstract ⇱

Europe - along with much of the developing world - is ready to implement a new and robust regime of data protection. The IT industry is carefully considering the challenges and the opportunities that these new legal regulations may create. Data protection provides a pillar of trust necessary to nurture emerging services and products. Even so, concern has been expressed that the new rules could hinder innovation and create barriers to design and engineering. Some companies believe the regulatory bar has now been set too high and that data protection will create substantial problems. In this talk veteran privacy expert Simon Davies discusses whether the proposed rules have struck the right formula.

Simon Davies is the Founder of Privacy International and Associate Director of LSE Enterprise. He has been a Visiting Fellow in Law at both the University of Greenwich and the University of Essex, and spent 13 years at LSE, where he taught the groundbreaking MSc Masters course in “Privacy & Data Protection”. He is also co-director of LSE’s Policy Engagement Network. Simon Davies is widely acknowledged as one of the most influential data protection and internet rights experts in the world and is a pioneer of the international privacy arena. His work in consumer rights and technology policy has spanned over 25 years and has directly influenced the development of law and public policy in more than 40 countries. He has advised a wide range of corporate, government and professional bodies, including the United Nations High Commissioner for Refugees. Recently, Simon Davies has been tasked by cross-party rapporteurs of the European Parliament to conduct a wide-ranging external assessment of the European Commission's proposed reforms to the EU data protection framework. He brings a unique interface with global stakeholders, from major international corporations to government and civil society.
Slides

15 May 2013
Speaker: Andrea Polini (ISTI CNR)
Title: ASSERT Enabled Marketplace

Abstract ⇲

Abstract ⇱

Abstract ⇱

Platform providers establish marketplace ecosystems to sell to end users services and applications running on the platform. Very prominent examples of these marketplaces are the Google Play Store and Apple AppStore, among others. Application Developers can use these marketplaces to offer services and applications to end users. Advanced Security Service cERTificate (ASSERT) for SOA (ASSERT4SOA) is a Framework designed to associate certificates of Security properties with the applications and services. This framework offers services like verification of ASSERTs and matching those ASSERTs to Security Properties specified in an appropriate query language. ASSERT Enabled Marketplace is a prototype to qualitatively evaluate and illustrate the use of ASSERT4SOA Framework in a marketplace which sells business applications, which have certificates issued for certain security properties. This marketplace is designed based on a typical user story of buying business applications based on the organization’s security requirements, comparing and choosing the best option based on the requirements.
Slides

05 April 2013
Speaker: Luca Maria Cassano (ISTI CNR)
Title: Analysis and Test of the Effects of Single Event Upsets in the Configuration Memory of SRAM-based FPGAs

Abstract ⇲

Abstract ⇱

Abstract ⇱

SRAM-based FPGAs are increasingly relevant in a growing number of safety-critical application fields, ranging from automotive to aerospace. These application fields are characterized by a harsh radiation environment that can cause the occurrence of Single Event Upsets (SEUs) in digital devices. Designing safety-critical applications requires accurate methodologies to evaluate the system’s sensitivity to SEUs as early as possible during the design process. Moreover it is necessary to detect the occurrence of SEUs during the system life-time. In this talk we present a set of software tools that could be used by designers of SRAM-based FPGA safety-critical applications to assess the sensitivity to SEUs of the system and to generate test patterns for in-service testing. In particular three tools have been designed and developed: (i) ASSESS: Accurate Simulator of SEuS affecting the configuration memory of SRAM-based FPGAs; (ii) UA2TPG: Untestability Analyzer and Automatic Test Pattern Generator for SEUs Affecting the Configuration Memory of SRAM-based FPGAs; and (iii) GABES: Genetic Algorithm Based Environment for SEU Testing in SRAM-FPGAs.
Slides

13 March 2013
Speaker: Franco Mazzanti (ISTI CNR)
Title: Abstract Modelling and On-the-fly model checking

Abstract ⇲

Abstract ⇱

Abstract ⇱

The seminar will present the underlying basic ideas and the current status of the UMC/FMC/CMC/VMC modellling and verification framework developed at ISTI. A railway scenario will be used to illustrate in more detail the features of UMC.
Slides

20 February 2013
Speaker: Stefano Ricci (Università degli Studi di Roma “La Sapienza”)
Title: L'uso delle Reti di Petri per la modellazione della circolazione ferroviaria

Abstract ⇲

Abstract ⇱

Abstract ⇱

Cenni sulla Teoria delle Reti di Petri. Algebra e formalismo grafico delle Reti di Petri, Formulazione analitico matriciale, Situazioni fondamentali in una Rete di Petri,Tipologie di Reti di Petri, Estensioni della teoria delle Reti di Petri e problemi di standardizzazione. Le Reti di Petri utilizzabili nelle applicazioni ferroviarie. Reti di Petri estese, Proprietà estese delle marche, Proprietà estese delle transizioni, Proprietà estese dei posti , Reti di Petri e modelli gerarchici, Reti di Petri colorate. Architettura dei modelli per le analisi dell'esercizio ferroviario. Obiettivi e limiti dei modelli di simulazione, Struttura “object oriented”, Reti estese mediante programmazione, Reti colorate e finestra di simulazione, Limiti nella possibilità di rappresentazione e simulazione, Elementi rappresentati e Classi costitutivi dei modelli, Funzionamento dei modelli. Esempio di modello per la tratta Roma-Formia. Descrizione della linea fini della sua rappresentazione nel modello, Cenni sui sistemi di comando e controllo, Rappresentazione nel modello, Simulazione dell'orario teorico nelle ore di punta, Simulazioni in regime perturbato nelle ore di punta, Effetto della cinematica del treno sulle simulazioni. Altre possibili applicazioni. Analisi dei passaggi a livello, Valutazione della capacità di circolazione nei nodi, Risoluzione dei conflitti ai nodi. Conclusioni. Obiettivi raggiunti, lacune da colmare, applicazioni possibili, sviluppi futuri.
Slides


2012 Seminars

19 December 2012
Speaker: Alessio Ferrari (ISTI CNR)
Title: Using Collective Intelligence to Detect Natural Language Pragmatic Ambiguities

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding “concept paths” within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the presentation to illustrate the soundness of the proposed strategy.
Slides

19 December 2012
Speaker: Alessio Ferrari (ISTI CNR)
Title: Using Collective Intelligence to Detect Natural Language Pragmatic Ambiguities

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding “concept paths” within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the presentation to illustrate the soundness of the proposed strategy.
Slides

05 December 2012
Speaker: Andrea Polini (ISTI CNR)
Title: Run-time Failure Forecasting for Dynamically Evolving Systems

Abstract ⇲

Abstract ⇱

Abstract ⇱

no abstract.
Slides

21 November 2012
Speaker: Mieke Massink (ISTI CNR)
Title: Analysing Robot Swarm Decision-making with Bio-PEPA

Abstract ⇲

Abstract ⇱

Abstract ⇱

A formal approach to analyse swarm robotics systems is presented based on Bio-PEPA. Bio-PEPA is a process algebraic language originally developed to analyse biochemical systems. Its main advantage is that it allows different kinds of analyses of a swarm robotics system starting from a single description. In general, to carry out different kinds of analysis, it is necessary to develop multiple models, raising issues of mutual consistency. With Bio-PEPA, instead, it is possible to perform stochastic simulation, fluid flow analysis and statistical model checking based on the same system specification. This reduces the complexity of the analysis and ensures consistency between analysis results. Bio-PEPA is well suited for swarm robotics systems, because it lends itself well to modelling distributed scalable systems and their space-time characteristics. We demonstrate the validity of Bio-PEPA by modelling collective decision-making as an emergent phenomenon in a swarm robotics system and we evaluate the result of different analyses.
Slides

07 November 2012
Speaker: Giorgio Oronzo Spagnolo (ISTI CNR)
Title: Product Line Engineering Applied to CBTC Systems Development

Abstract ⇲

Abstract ⇱

Abstract ⇱

Communications-based Train Control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities. Furthermore, every installed system, developed by a different company, varies in extent, scope and number of them. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. The paper that will be presented into seminar reports intermediate results in an effort aimed at defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The adopted methodology is discussed.
Slides

14 September 2012
Speaker: Alessio Ferrari (ISTI CNR)
Title: Using Collective Intelligence to Detect Natural Language Pragmatic Ambiguities

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding “concept paths” within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the presentation to illustrate the soundness of the proposed strategy.
Slides


2011 Seminars

Friday, 25 November 2011
Speaker: Erik de Vink (Eindhoven University of Technology & CWI Amsterdam, The Netherlands)
Title: Analysis of aa-tRNA competition: An application of Prism in systems biology

Abstract ⇲

Abstract ⇱

Abstract ⇱

We present a formal analysis of ribosome kinetics using probabilistic model checking with the tool Prism. We compute different parameters of the model, like probabilities of translation errors and average insertion times per codon. The model predicts a strong correlation to the quotient of the concentrations of the so-called cognate and near-cognate tRNAs, in accord with experimental findings and other studies. Using piecewise analysis of the model, we are able to give an analytical explanation of this observation. Joint work with Dragan Bosnacki (TU/e) and Tessa Pronk (RIVM).
Slides

14 November 2011
Speaker: Jorge Fox (ERCIM Fellow)
Title: Dynamic Variability in Families of Clouds

Abstract ⇲

Abstract ⇱

Abstract ⇱

The use of a cloud service requires a company to trust the vendor to comply with given Service-level Agreements (SLA). This work proposes a framework for modelling and maintaining Quality of Service levels expressed as SLA's through the definition of families of clouds as software service line organisations. By systematically exploiting the commonalities within related cloud systems while managing variations for specific customers, we relate variability to SLA's facilitating their monitoring, controlling and enforcement. Coupling the abstraction capabilities of product line approaches and SLA's to ensure Quality of Service in Cloud Computing is a novel approach, which offers the possibility to support dynamic negotiation of QoS parameters. In the long run, our work aims to provide a generic framework for non-functional requirements enforcement in the Cloud.
Slides

7 November 2011
Speaker: Maurice ter Beek (ISTI CNR)
Title: Modelling and Analysing Variability in Product Families

Abstract ⇲

Abstract ⇱

Abstract ⇱

We propose an emerging solution technique and a support tool for modelling and analysing variability in product families. First we illustrate how to manage variability in a formal framework consisting of a Modal Transition System (MTS) and an associated set of formulae expressed in the variability and action-based branching-time temporal logic vaCTL. We then introduce the tool VMC, which accepts as input the specification of a product family in a CCS-like process algebra, possibly with an additional set of variability constraints. We show how VMC can be used to automatically generate all valid products of this family, defined in the same process algebra, as well as to visualise the family (products) as modal (labelled) transition systems. Finally, we show how VMC can efficiently verify functional properties expressed as formulae in vaCTL, over products and families alike, by means of its on-the-fly model-checking algorithm.
This is joint work with FMT members Patrizia Asirelli, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, and Aldi Sulova.
Slides

25 October 2011
Speaker: Peter Herrmann (Department of Telematics (ITEM) - Norwegian University of Science and Technology (NTNU)
Title: Model-based Engineering of Distributed Systems with SPACE and Arctis

Abstract ⇲

Abstract ⇱

Abstract ⇱

Model-based software engineering techniques are suited for the rapid and cheap service development. Our approach SPACE and its tool set Arctis use collaborative models each describing a possibly distributed sub-service instead of a single physical component. An advantage of this proceeding is its high potential for reuse since many distributed systems in a certain domain are realized by a limited number of sub-services which, however, are composed in quite different ways. Such, we could achieve a reuse rate of about 70% in average for our developments.
As a modeling technique, we use UML2 collaborations and activities enabling service specifications in an intelligible graphical notation. Our modeling tool Arctis transforms the collaborative models into Java code running among others on J2EE, Sun SPOTS and Google Android telephones. We can further apply model checking to analyze the models for design errors. This verification is carried out in a way that the user does not need any knowledge about the formalism as the errors are directly visualized on the graphical descriptions.
My presentation will introduce SPACE and Arctis and discuss model transformation and model checker-based analysis..
Slides

17 October 2011
Speaker: Alessio Ferrari (ISTI CNR)
Title: Adoption of SysML by a Railway Signaling Manufacturer

Abstract ⇲

Abstract ⇱

Abstract ⇱

This talk reports the experience of a railway signaling manufacturer in introducing the SysML notation within its development process by means of the TOPCASED tool. Though the tool was later substituted by MagicDraw, the experience was useful to understand the potentials of the notation for requirements formalization and analysis, together with the advantages and drawbacks of using an open-source tool in an industrial setting.
Slides

14 October 2011
Speaker: Erik de Vink (Eindhoven University of Technology & CWI Amsterdam, The Netherlands)
Title: Modeling Dynamic System Adaptation with Paradigm

Abstract ⇲

Abstract ⇱

Abstract ⇱

Dynamic system evolution of cooperating software components can be modeled in the Paradigm language. Paradigm provides layers of granularity, allowing to describe component interaction at a higher level of abstraction. A special component called McPal gradually changes the interaction at the abstract level, guiding the dynamics of the system from the old AsIs situation into the new ToBe situation without the need for a system shutdown.
Paradigm models can be systematically translated into the process algebra mCRL2. An extensive toolset is available for mCRL2, including LTS visualization and symbolic model checking. Thus, exploiting this connection, tool-supported verification of system migration has become within reach. The approach is illustrated for a simple producer/consumer example. If time allows a demo of the use of mCRL2 is included in this talk.
Joint work with Luuk Groenewegen and Suzana Andova.
Slides

7 October 2011
Speaker: Diego Latella (ISTI-CNR)
Title: FuTS - A Uniform Framework for the Definition of Stochastic Process Languages

Abstract ⇲

Abstract ⇱

Abstract ⇱

Process Algebras are one of the most successful formalisms for modeling concurrent systems and proving their properties. Due to the growing interest in the analysis of shared-resource systems, stochastic process algebras have received great attention. The main aim has been the integration of qualitative descriptions with quantitative (especially performance) ones in a single mathematical framework by building on the combination of Labeled Transition Systems and Continuous-Time Markov Chains. In this talk a unifying framework is introduced for providing the semantics of some of the most representative stochastic process languages; aiming at a systematic understanding of their similarities and differences. The used unifying framework is based on so called State to Function Labelled Transition Systems, FuTSs for short, that are state-transition structures where each transition is a triple of the form (s,α,P). The first and the second components are the source state and the label of the transition while the third component, P, is the continuation function associating a value of a suitable type to each state s’. A non-zero value may represent the cost to reach s’ from s via α. The FuTSs framework is used to model represenative fragments of major stochastic process calculi and the costs of continuation function do represent the rate of the exponential distribution characterizing the execution time of the performed action. In the talk, first the FuTSs are introduced and then the semantics for a simple language used to directly describe (unlabeled) CTMCs.
Slides

5 October 2011
Speaker: Anatoliy Gorbenko (National Aerospace University “KhAI”, Kharkiv, Ukraine)
Title: FuTS - A Uniform Framework for the Definition of Stochastic Process Languages

Abstract ⇲

Abstract ⇱

Abstract ⇱

Dealing with uncertainty inherent in the very nature of service-oriented architectures, is one of the main challenges in building dependable service architectures. This uncertainty needs to be treated as a threat in a way similar to and in addition to faults, errors and failures, traditionally dealt with by the research community. The lack of sufficient evidence about the characteristics of the communication medium, components and their possible dependencies makes it extremely difficult to achieve and predict (composite) service dependability which can vary over a wide range in a very random manner. This uncertainty of services running over the Internet and clouds exhibits itself through the unpredictable response times of messages and data transfers, difficulty to diagnose the root cause of failures, unknown common mode failures, etc.
Slides

27 September 2011
Speaker: Joost-Pieter Katoen (RWTH Aachen University, Germany)
Title: Timed Automata as Observers of Stochastic Processes

Abstract ⇲

Abstract ⇱

Abstract ⇱

In this talk, we will argue that (deterministic) timed automata are a natural specification formalism for practically relevant measures on stochastic processes. It will be discussed how DTA specifications can be checked on continuous-time Markov chains, an important class of stochastic processes used in the performance and dependability community, by using a product construction. We'll provide encouraging empirical results for checking single-clock DTA specifications and indicate how parallelization as well as bisimulation minimization can be naturally exploited in this setting. Finally, we shortly discuss the model checking of DTA specifications on a richer class of stochastic processes: continuous-time Markov decision processes (CTMDPs).
Slides


Past Seminars
Issues of Domain Engineering (Prof. Dines Bjorner)
Integration of Decision Procedures: State of the Art (Prof. Zohar Manna)
What is an Algorithm? (Prof.Yuri Gurevich)
Policies, Presence and Availability Services (Prof. Jorge Lobo)
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol (Prof. Jeremy Sproston)
Furthermore the FM&&T Group established the ERCIM FMICS Working Group in 1996.