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
Ojeda-Hernández DD
(2023)
Screening, synthesis optimization, and scaling-up of phytopathogen antifungals derived from natural hydroxycinnamic acids.
in 3 Biotech
Nielsen C
(2015)
Systems of Systems Engineering Basic Concepts, Model-Based Techniques, and Research Directions
in ACM Computing Surveys
Woodcock J
(2009)
Formal methods Practice and experience
in ACM Computing Surveys
Chang W
(2020)
Development Automation of Real-Time Java Model-Driven Transformation and Synthesis
in ACM Transactions on Embedded Computing Systems
Perna J
(2011)
Correct hardware synthesis An algebraic approach
in Acta Informatica
Helfenstein J
(2022)
An approach for comparing agricultural development to societal visions.
in Agronomy for sustainable development
Perna J
(2009)
Mechanised Wire-wise Verification of Handel-C Synthesis
in Electronic Notes in Theoretical Computer Science
Gleirscher M
(2021)
Proceedings First Workshop on Applicable Formal Methods Preface
in Electronic Proceedings in Theoretical Computer Science
Paige R
(2009)
Editorial
in Formal Aspects of Computing
Zhao H
(2021)
Learning safe neural network controllers with barrier certificates
in Formal Aspects of Computing
Freitas L
(2009)
FDR Explorer
in Formal Aspects of Computing
Oliveira M
(2009)
A UTP semantics for Circus
in Formal Aspects of Computing
Kroening D
(2011)
Editorial
in Formal Aspects of Computing
Gleirscher M
(2021)
RiskStructures : A design algebra for risk-aware machines
in Formal Aspects of Computing
Oliveira M
(2013)
Unifying theories in ProofPower-Z
in Formal Aspects of Computing
Woodcock J
(2012)
Editorial
in Formal Aspects of Computing
Cheng S
(2015)
Using formal reasoning on a model of tasks for FreeRTOS
in Formal Aspects of Computing
Cavalcanti A
(2014)
Test-data generation for control coverage by proof
in Formal Aspects of Computing
Liu Z
(2011)
Editorial
in Formal Aspects of Computing
Proietti M
(2017)
Editorial
in Formal Aspects of Computing
Mota A
(2015)
Model checking CML: tool development and industrial applications
in Formal Aspects of Computing
Woodcock J
(2015)
Editorial
in Formal Aspects of Computing
Cavalcanti A
(2013)
The Safety-Critical Java memory model formalised
in Formal Aspects of Computing
Wei K
(2013)
Modelling temporal behaviour in complex systems with Timebands
in Formal Methods in System Design
Ye K
(2015)
Model checking of state-rich formalism by linking to $$CSP\,\Vert \,B$$ C S P ? B
in International Journal on Software Tools for Technology Transfer
Foster S
(2021)
Automated verification of reactive and concurrent programs by calculation
in Journal of Logical and Algebraic Methods in Programming
Cavalcanti A
(2013)
Safety-critical Java programs from Circus models
in Real-Time Systems
Freitas L
(2009)
Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository
in Science of Computer Programming
Perna J
(2012)
Mechanised wire-wise verification of Handel-C synthesis
in Science of Computer Programming
Butterfield A
(2009)
Mechanising a formal model of flash memory
in Science of Computer Programming
Freitas L
(2009)
POSIX file store in Z/Eves: An experiment in the verified software repository
in Science of Computer Programming
Mishra S
(2023)
'Cyclic syndrome' of arrears and efficiency of Indian judiciary.
in SN business & economics
Ye K
(2021)
Probabilistic modelling and verification using RoboChart and PRISM
in Software and Systems Modeling
Mistry J
(2014)
Adapting FreeRTOS for multicores: an experience report ADAPTING FREERTOS FOR MULTICORES: AN EXPERIENCE REPORT
in Software: Practice and Experience
Foster S
(2013)
Unifying Theories of Programming and Formal Engineering Methods
Oliveira M
(2013)
Software Engineering and Formal Methods
Butterfield A
(2009)
State Visibility and Communication in Unifying Theories of Programming
Foster S
(2017)
Unifying Theories of Programming
Dos Santos O
(2010)
Formal Methods for Components and Objects
Perna J
(2010)
Unifying Theories of Programming
Woodcock J
(2016)
Formal Methods: Foundations and Applications
Ribeiro P
(2017)
Unifying Theories of Programming
Woodcock J
(2012)
Features of CML: A formal modelling language for Systems of Systems
Cavalcanti A
(2015)
Theoretical Aspects of Computing - ICTAC 2015
Esterle L
(2021)
Verification and Uncertainties in Self-integrating System
Fitzgerald J
(2013)
Industrial Deployment of System Engineering Methods
Woodcock J
(2013)
Unifying Theories of 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 |