David Ebo Adjepon‐Yamoah

Paulius Stankaitis, Alexei Iliasov, David Adjepon-Yamoah et al.

Event-B is one of more popular notations for model-based, proof driven specification. It offers a fairly high-level mathematical lan- guage based on FOL and ZF set theory and an economical yet expres- sive modelling notation. Model correctness is established by discharging proving a number conjectures constructed via a syntactic instantiation of schematic conditions. A large proportion of provable conjectures re- quires proof hints from a user. For larger models this becomes extremely onerous as identical or similar proofs have to be repeated over and over, especially after model refactoring stages. In the paper we briefly present a new Rodin Platform proof back-end based on the Why3 umbrella prover.

David Ebo Adjepon-Yamoah

This paper reports on our definition of guidelines for managing global software development (GSD) that implements the specific practice - manage requirements changes - of the Capability Maturity Model Integration (CMMI) Level 2. The guidelines present a model for change management and traceability that supports the implementation of the specific CMMI Level 2 goal. Also, to support the effective management of the system engineering processes, an adaptation of the Project Management Body of Knowledge (PMBOK) process group (PG) for project life-cycle practices is provided. We introduce a cloud-based Reactive Middleware which provides services for managing GSD projects towards dependable change management and traceability.