creators_name: Iliasov, Alexei creators_id: "Alexei Iliasov" type: book_section datestamp: 2012-03-06 18:52:06 lastmod: 2012-03-06 18:52:06 metadata_visibility: show title: Augmenting formal development with use case reasoning ispublished: pub subjects: Event-Bsemantics subjects: deploy_method subjects: deploy_tooldev subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplugins full_text_status: public abstract: State-based methods for correct-by-construction software development rely on a combination of safety constraints and refinement obligations to demonstrate design correctness. One prominent challenge, especially in an industrial setting, is ensuring that a design is adequate: requirements compliant and fit for purpose. The paper presents a technique for augmenting state-based, refinement-driven formal developments with reasoning about use case scenarios; in particular, it discusses a way for the derivation of formal verification conditions from a high-level, diagrammatic language of use cases, and the methodological role of use cases in a formal modelling process. date: 2012 date_type: published publisher: Springer refereed: TRUE book_title: Proc. of the 17th International Conference on Reliable Software Technologies (Ada-Europe 2012). Stockholm, Sweden. June 11-15, 2012. citation: Iliasov, Alexei (2012) Augmenting formal development with use case reasoning. In: Proc. of the 17th International Conference on Reliable Software Technologies (Ada-Europe 2012). Stockholm, Sweden. June 11-15, 2012. Springer. document_url: http://deploy-eprints.ecs.soton.ac.uk/372/1/AE-final-2012-main.pdf