Systems Development: Domain-Specific Modelling

Lead Research Organisation: University of York
Department Name: Computer Science

Abstract

Traditionally, engineers use their experience in a problem domain and their knowledge of science and mathematics to find suitable solutions to a problem. They develop candidate solutions by building appropriate mathematical models, which they then analyse and test, using tools wherever possible. In the same way, system engineering is becoming ever-more dependent on modelling and a range of different tools and techniques are being used. These models are used to solve the problem in terms familiar to the domain expert, but in doing so they leave a wide gap between the domain model and the implementation technology. In this context, the project will address three challenges:(1) How do we use automated tools to support a variety of different modelling languages in a consistent manner?(2) How do we integrate them into existing development processes?(3) How do we obtain requirements traceability?We will develop new approaches using domain-specific modelling processes and will provide effective tool support. The project will be carried out in partnership with the National Physical Laboratory, and will be validated by experimentation on end-to-end case studies provided by NPL. Prototype tools will be ready for further development and exploitation as production-quality tools at the end of the project.

Publications

10 25 50
publication icon
Mota A (2015) Model checking CML: tool development and industrial applications in Formal Aspects of Computing

publication icon
Oliveira M (2013) Unifying theories in ProofPower-Z in Formal Aspects of Computing

publication icon
Oliveira M (2009) A UTP semantics for Circus in Formal Aspects of Computing

publication icon
Paige R (2009) Editorial in Formal Aspects of Computing

publication icon
Perna J (2012) Mechanised wire-wise verification of Handel-C synthesis in Science of Computer Programming

 
Description This project developed an approach to the type analysis of scientific programming languages, such as those supported by MATLAB and its close open-source cousin Octave. The MATLAB programming language has a notion of type, but its function headers do not carry type constraints. This is because both operators and functions are heavily overloaded and can produce meaningful results for almost any combination of types. However, the lack of type information limits the programmer's confidence in their artefacts since they have no way to express and check intent. Moreover, for certain combinations of types the operators and built-in functions will produce run-time errors, which clearly need to be avoided. Our approach has more in common with established notions from formal methods, such as predicate transformers and refinement, than classical type-checking. Type interfaces for functions are expressed predicatively over types, and analysis is performed to show that a) function preconditions are respected by the arguments supplied at the instance of their use; b) user supplied type assertions hold; and c) the function body satisfies its type interface. We have implemented the proposals using Microsoft Research's Z3 SMT solver.
Exploitation Route Our software tool may be of use to those working with MATLAB specifications for scientific programming.
Sectors Aerospace, Defence and Marine,Agriculture, Food and Drink,Chemicals,Creative Economy,Digital/Communication/Information Technologies (including Software),Electronics,Energy,Environment,Financial Services, and Management Consultancy,Manufacturing, including Industrial Biotechology,Pharmaceuticals and Medical Biotechnology,Transport

 
Description EMRP
Amount € 100,000 (EUR)
Funding ID NEW06-REG4(UoY) 
Organisation European Association of National Metrology Institutes (EURAMET) 
Sector Charity/Non Profit
Country Germany
Start 05/2014 
End 05/2015