Formal specification and verification of TCP extended with the Window Scale Option
We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With the aid of our µCRL specification and the LTSmin toolset, we verify that our specification of unidirectional TCP Data Transfer extended with the ...
An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis
A fault-tolerant routing algorithm in Network-on-Chip (NoC) architectures provides adaptivity for on-chip communications. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other ...
Assertion-based monitoring in practice Checking correctness of an automotive sensor interface
This paper provides an evaluation of the assertion-based monitoring technology for mixed-signal systems applied to a real-world case study from the automotive domain. We first motivate the case study by presenting the state-of-the-practice verification ...
Randomised testing of a microprocessor model using SMT-solver state generation
We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on randomly chosen instructions against real chips from several manufacturers.The model and our intended application involve precise timing information ...
Improving static analyses of C programs with conditional predicates
Static code analysis is increasingly used to guarantee the absence of undesirable behaviors in industrial programs. Designing sound analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide ...