2014-08-26: Seminar Prof Vladimir Estivill-Castro on Correctness by Construction with Logic-Labelled Finite-State Machines – Comparison with Event-B

Formal methods have seen emergent success recently with the deployment of Event-B. However, Event-B explicitly postulates that models there are not executable. This seems to contradict the parallel emergence of model-driven development (MDD). We show here that logic-labelled finite-state machines (LLFSMs) are effective in carrying out the “correct from construction” agenda of formal methods such as Event-B and simultaneously achieve the aims of MDD. As a result, we obtain models that are directly interpretable, compilable, and executable enabling traceability, transparency and rapid maintainability; while at the same time enabling simulation, validation and formal verification with model checking. Moreover, the Event-B capacity to develop closed models is also very natural with arrangements of LLFSMs; and therefore further safety analysis such as failure-mode effects analysis (FMEA) can be performed. We demonstrate this with two well-known examples in the literature.

2014-08-25 Seminar Dr Han on Next-Generation Storage and Its Software

Recently, storage devices have been greatly improved in terms of both bandwidth and latency by using non-volatile memories such as Flash and PRAM. However, traditional storage software stack such as operating systems and database systems becomes major performance bottleneck since they are optimized for hard disk drives and they are not suitable for new storage devices. We call this phenomenon "slow software on fast storage". For the seminar, histories of storage devices will be given in terms of interconnection and bandwidth. Then, I will show an example of software optimizations for fast storage devices, and describe our current work about virtual memory of operating systems. Finally, I'll present our future work about application-level optimizations for fast storage devices.

2014-08-23 Doctorate Awarded
David Cock has received his Doctorate. He worked to extend seL4's assurance case to non-functional security properties. Established an empirical approach to detecting and mitigating covert and side channels.

2014-08-13 Seminar Roy on A CSP-theoretic framework of checking conformance of business processes

In this talk, we tackle the problem of conformance checking which > verifies if the event logs (observed) match/fit the reference (arbitrary) process. We use concepts from Communicating Sequential Processes (CSP), which facilitates automated analysis using PAT toolkit. By this technique one can identify all the logs which cannot be properly replayed on the process. We illustrate our approach with an example. Finally, we introduce some metrics based on conformance checking. They are related to fitness, closeness, and appropriateness of the event logs vis-a-vis reference process models. We further indicate that such a framework can be used to tackle the problem of both static and run-time compliance checking for business processes. Our work is motivated by user friendly need of employing easy input technique of models and keeping the model checking work at the back-end.

2014-08-05: Podcast Interview with Len Bass
Architect Len Bass and author of Software Architecture in Practice has been interviewed for a podcast .