Sciweavers

APCCM
2009
14 years 19 days ago
Conceptional Modeling and Analysis of Spatio-Temporal Processes in Biomolecular Systems
In life science, deeper understanding of biomolecular systems is acquired by computational modeling and analysis. For the modeling of several kinds of reaction networks, e.g. sign...
Andreas Schäfer, Mathias John
WOA
2007
14 years 20 days ago
Declarative representation of curricula models: an LTL- and UML-based approach
Abstract—In this work, we present a constrained-based representation for specifying the goals of “course design”, that we call curricula model, and introduce a graphical lang...
Matteo Baldoni, Cristina Baroglio, Giuseppe Berio,...
EUMAS
2006
14 years 27 days ago
A Metamodel for Verifying Institutions
To investigate the interdependencies existing among deontic positions (like powers and obligations) and the ontology defined by an institution, we have proposed to model instituti...
Francesco Viganò
APLAS
2005
ACM
14 years 1 months ago
A Parametric Model for the Analysis of Mobile Ambients
In this paper we propose a new parametric abstract finite model of Mobile Ambients able to express several properties on processes. The model can be used for the analysis of these...
Dino Distefano
ICCD
1995
IEEE
109views Hardware» more  ICCD 1995»
14 years 3 months ago
Verifying the performance of the PCI local bus using symbolic techniques
Symbolic model checking is a successful technique for checking properties of large finite-state systems. This method has been used to verify a number of real-world hardware desig...
Sérgio Vale Aguiar Campos, Edmund M. Clarke...
SPIN
2000
Springer
14 years 3 months ago
Verification and Optimization of a PLC Control Schedule
Abstract. We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this wor...
Ed Brinksma, Angelika Mader
MOVEP
2000
167views Hardware» more  MOVEP 2000»
14 years 3 months ago
Model Checking: A Tutorial Overview
We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an analysis of the Needham-Schroeder p...
Stephan Merz
DSN
2004
IEEE
14 years 3 months ago
Verifying Web Applications Using Bounded Model Checking
The authors describe the use of bounded model checking (BMC) for verifying Web application code. Vulnerable sections of code are patched automatically with runtime guards, allowin...
Yao-Wen Huang, Fang Yu, Christian Hang, Chung-Hung...
TACAS
1997
Springer
132views Algorithms» more  TACAS 1997»
14 years 3 months ago
Test Generation for Intelligent Networks Using Model Checking
We study the use of model checking techniques for the generation of test sequences. Given a formal model of the system to be tested, one can formulate test purposes. A model checke...
André Engels, Loe M. G. Feijs, Sjouke Mauw
CAV
1998
Springer
147views Hardware» more  CAV 1998»
14 years 3 months ago
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking
An implementation of an out-of-order processing unit based on Tomasulo's algorithm is formally verified using compositional model checking techniques. This demonstrates that f...
Kenneth L. McMillan