Agile Model-Based Development Using UML-RSDS

17.8.3 Requirements formalisation -- 17.8.4 Validation and verification -- 18: System Verification -- 18.1 Class diagram correctness -- 18.2 State machine correctness -- 18.3 Use case correctness -- 18.3.1 Definedness and determinacy of expressions -- 18.3.2 Confluence checks -- 18.4 Correctness by construction -- 18.5 Synthesis of B AMN -- 18.6 Synthesis of SMV -- 19: Reactive System Development with UML-RSDS -- 19.1 Constraint-based specification of reactive systems -- 19.2 State machines -- 19.3 Interactions -- 19.4 Reactive transformations -- 19.4.1 Case study: football player -- 20: Enterprise Systems Development with UML-RSDS -- 20.1 EIS synthesis -- 20.2 Example EIS application: bank accounts system -- 20.2.1 Client tier -- 20.2.2 Presentation tier -- 20.2.3 Business tier -- 20.2.4 Integration tier -- 21: Applications of UML-RSDS in Education and Industry -- 21.1 Teaching using UML-RSDS -- 21.2 Case study 1: FIXML code generation -- 21.2.1 Solution -- 21.2.2 Outcome -- 21.3 Case study 2: Electronic health records (EHR) analysis and migration -- 21.3.1 Solution -- 21.3.2 Outcome -- 21.4 Case study 3: Financial risk evaluation -- 21.5 Published case studies -- A: UML-RSDS Syntax -- A.1 OCL expression syntax -- A.2 Activity language syntax -- B: UML-RSDS tool architecture and components -- C: Key principles of UML-RSDS -- Index