Sciweavers

ICFEM
2007
Springer
13 years 8 months ago
Automating Refinement Checking in Probabilistic System Design
Abstract. Refinement plays a crucial role in "top-down" styles of verification, such as the refinement calculus, but for probabilistic systems proof of refinement is a pa...
Carlos Gonzalia, Annabelle McIver
ICFEM
2007
Springer
13 years 8 months ago
From Model-Based Design to Formal Verification of Adaptive Embedded Systems
Rasmus Adler, Ina Schaefer, Tobias Schüle, Er...
ICFEM
2007
Springer
13 years 8 months ago
Testing for Refinement in CSP
Abstract. CSP is a well-established formalism for modelling and verification of concurrent reactive systems based on refinement. Consolidated denotational models and an effective t...
Ana Cavalcanti, Marie-Claude Gaudel
ICFEM
2007
Springer
13 years 10 months ago
Formal Engineering of XACML Access Control Policies in VDM++
We present a formal, tool-supported approach to the design and maintenance of access control policies expressed in the eXtensible Access Control Markup Language (XACML). Our aim is...
Jeremy Bryans, John S. Fitzgerald
ICFEM
2007
Springer
13 years 10 months ago
Machine-Assisted Proof Support for Validation Beyond Simulink
Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we sh...
Chunqing Chen, Jin Song Dong, Jun Sun 0001
ICFEM
2007
Springer
13 years 10 months ago
Model Checking with SAT-Based Characterization of ACTL Formulas
Bounded semantics of LTL with existential interpretation and that of ECTL (the existential fragment of CTL), and the characterization of these existentially interpreted properties ...
Wenhui Zhang
ICFEM
2007
Springer
13 years 10 months ago
Formalizing SANE Virtual Processor in Thread Algebra
Thuy Duong Vu, Chris R. Jesshope