Mohammadsadegh Dalvandi

Dr Sadegh Dalvandi


My publications

Publications

Dalvandi Mohammadsadegh, Dongol Brijesh (2019) Towards Deductive Verification of C11 Programs with Event-B and ProB, Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019) Association for Computing Machinery (ACM)
This paper introduces a technique for modelling and verifying
weak memory C11 programs in the Event-B framework.
We build on a recently developed operational semantics for
the RAR fragment of C11, which we use as a top-level abstraction.
In our technique, a concrete C11 program can be
modelled by refining this abstract model of the semantics.
Program structures and individual operations are then introduced
in the refined machine and can be checked and
verified using available Event-B provers and model checkers.
The paper also discusses how ProB model checker can be
used to validate the Event-B model of C11 programs. We applied
our technique to the C11 implementation of Peterson?s
algorithm, where we discovered that the standard invariant
used to characterise mutual exclusion is inadaquate. We
therefore propose and verify new invariants necessary for
characterising mutual exclusion in a weak memory setting.
Dghaym Dana, Dalvandi Mohammadsadegh, Poppleton Michael, Snook Colin (2019) Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B, International Journal on Software Tools for Technology Transfer Springer Verlag
We demonstrate refinement-based formal development of the hybrid, ?fixed virtual block? approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification?s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.
Fathabadi Asieh Salehi, Dalvandi Mohammadsadegh, Butler Michael, Al-Hashimi Bashir M. (2019) Verifying Cross-layer Interactions through Formal Model-based Assertion Generation, IEEE Embedded Systems Letters Institute of Electrical and Electronics Engineers (IEEE)
Cross-layer runtime management (RTM) frameworks for embedded systems provide a set of standard APIs for communication between different system layers (i.e. RTM, applications and device) and simplify the development process by abstracting these layers. Integration of independently developed components of the system is an error-prone process that requires careful verification. In this paper, we propose a formal approach to integration testing through automatic generation of runtime assertions in order to test the implementation of the APIs. Our approach involves a formal model of the APIs, developed using the Event-B formal method which is automatically translated to a set of assertions and embedded in the existing implementation of APIs. The embedded assertions are used at runtime to check the correctness of the integration. This work was supported by the EPSRC PRiME Project (EP/K034448/1), www.prime-project.org.
Dalvandi Mohammadsadegh, Butler Michael, Fathabadi Asieh Salehi (2019) SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B, Proceedings of the Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019) Springer
The guarded atomic action model of Event-B allows it to be
applied to a range of systems including sequential, concurrent and distributed systems. However, the lack of explicit sequential structures in
Event-B makes the task of sequential code generation difficult. Scheduled
Event-B (SEB) is an extension of Event-B that augments models with
control structures, supporting incremental introduction of control structures in refinement steps. SEB-CG is a tool for automatic code generation
from SEB to executable code in a target language. The tool provides facilities for derivation of algorithmic structure of programs through refinement. The flexible and configurable design of the tool allows it to target
various programming languages. The tool benefits from xText technology for a user-friendly text editor together with the proving facilities of
Rodin platform for formal analysis of the algorithmic structure.