Sciweavers

IFM
2009
Springer
106views Formal Methods» more  IFM 2009»
14 years 5 months ago
An Introduction to Grammar Convergence
Ralf Lämmel, Vadim Zaytsev
IFM
2009
Springer
14 years 5 months ago
Verifying UML/OCL Operation Contracts
In current model-driven development approaches, software models are the primary artifacts of the development process. Therefore, assessment of their correctness is a key issue to e...
Jordi Cabot, Robert Clarisó, Daniel Riera
IFM
2009
Springer
107views Formal Methods» more  IFM 2009»
14 years 5 months ago
Realizability of Choreographies Using Process Algebra Encodings
Abstract. Service-oriented computing has emerged as a new programming paradigm that aims at implementing software applications which can be used through a network via the exchange ...
Gwen Salaün, Tevfik Bultan
IFM
2009
Springer
124views Formal Methods» more  IFM 2009»
14 years 5 months ago
Dynamic Path Reduction for Software Model Checking
We present the new technique of dynamic path reduction (DPR), which allows one to prune redundant paths from the state space of a program under verification. DPR is a very general...
Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiao...
ICFEM
2009
Springer
14 years 5 months ago
Supporting Reuse of Event-B Developments through Generic Instantiation
It is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal mo...
Renato Silva, Michael Butler
FORMATS
2009
Springer
14 years 5 months ago
Realizability of Real-Time Logics
Abstract. We study the realizability problem for specifications of reactive systems expressed in real-time linear temporal logics. The logics we consider are subsets of MITL (Metr...
Laurent Doyen, Gilles Geeraerts, Jean-Franç...
FORMATS
2009
Springer
14 years 5 months ago
Analyzing Real-Time Event-Driven Programs
Embedded real-time systems are typically programmed in low-level languages which provide support for event-driven task processing and real-time interrupts. We show that the model c...
Pierre Ganty, Rupak Majumdar
FORMATS
2009
Springer
14 years 5 months ago
Critical Paths in the Partial Order Unfolding of a Stochastic Petri Net
In concurrent real-time processes, the speed of individual components has a double impact: on the one hand, the overall latency of a compound process is affected by the latency of...
Anne Bouillard, Stefan Haar, Sidney Rosario
FORMATS
2009
Springer
14 years 5 months ago
On the Supports of Recognizable Timed Series
Recently, the model of weighted timed automata has gained interest within the real-time community. In a previous work, we built a bridge to the theory of weighted automata and intr...
Karin Quaas