Sciweavers

FMICS
2010
Springer
13 years 10 months ago
A Study of Shared-Memory Mutual Exclusion Protocols Using CADP
Mutual exclusion protocols are an essential building block of concurrent systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurr...
Radu Mateescu, Wendelin Serwe
FMICS
2010
Springer
14 years 19 days ago
Correctness of Sensor Network Applications by Software Bounded Model Checking
We investigate the application of the software bounded model checking tool CBMC to the domain of wireless sensor networks (WSNs). We automatically generate a software behavior mode...
Frank Werner, David Faragó
FMICS
2010
Springer
14 years 19 days ago
Range Analysis of Microcontroller Code Using Bit-Level Congruences
Bitwise instructions, loops and indirect data access pose difficult challenges to the verification of microcontroller programs. In particular, it is necessary to show that an indir...
Jörg Brauer, Andy King, Stefan Kowalewski
FMICS
2010
Springer
14 years 1 months ago
A Formal Model of Identity Mixer
Identity Mixer is an anonymous credential system developed at IBM that allows users for instance to prove that they are over 18 years old without revealing their name or birthdate....
Jan Camenisch, Sebastian Mödersheim, Dieter S...
FMICS
2010
Springer
14 years 1 months ago
Model Checking the FlexRay Physical Layer Protocol
Abstract. The FlexRay standard, developed by a cooperation of leading companies in the automotive industry, is a robust communication protocol for distributed components in modern ...
Michael Gerke 0002, Rüdiger Ehlers, Bernd Fin...
FMICS
2010
Springer
14 years 1 months ago
Embedded Network Protocols for Mobile Devices
Embedded networks for chip-to-chip networks are emerging as communication infrastructure in mobile devices. We present three novel embedded network protocols: a sliding window prot...
Despo Galataki, Andrei Radulescu, Kees Verstoep, W...
FMICS
2010
Springer
14 years 1 months ago
SMT-Based Formal Verification of a TTEthernet Synchronization Function
Abstract. TTEthernet is a communication infrastructure for mixedcriticality systems that integrates dataflow from applications with different criticality levels on a single network...
Wilfried Steiner, Bruno Dutertre