ENTRUST (ENgineering of TRUstworthy Self-adaptive sofTware) is the first tool-supported methodology for the engineering of high-integrity self-adaptive software systems and the dynamic generation of their assurance cases.
ENTRUST includes methods for the development of verifiable controllers for self-adaptive systems, for the generation of design-time and runtime assurance evidence, and for the runtime instantiation of an assurance argument pattern devised specifically for these systems.
Stages and key artefacts of the ENTRUST methodology.
ENTRUST is a joint work carried out by the departments of Computer Science, University of York, UK and Linnaeus University, SWE.
Further information about ENTRUST, can be found [here] (http://www-users.cs.york.ac.uk/~simos/ENTRUST).
###Prerequisites ENTRUST self-adaptive systems use verifiable controller and stochastic models, and formal assurance cases. The current version of ENTRUST is realised using the following technologies:
-
Controller models are specified as a network of interacting timed automata and are assessed at design-time for their correctness using [UPPAAL] (http://www.uppaal.org). At runtime, these models are executed by a [reusable virtual machine] (http://homepage.lnu.se/staff/daweaa/ActivFORMS/ActivFORMS.htm) (in ENTRUST_*/repo/com/activForms).
-
Stochastic models are parametric stochastic Markovian models and are specified in the [PRISM language] (http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction). At runtime, these models are verified using the probabilistic model checker PRISM (in ENTRUST_*/repo/org/modelchecker/PRISM).
-
Assurance cases are developed using the Goal Structuring Notation, a community standard widely used in industry for developing assurance cases (in ENTRUST_*/resources).
###Repository Structure
- Controller: A generic (abstract) ENTRUST controller including the necessary classes and instructions for developing an applicaiton-specific ENTRUST controller
- Examples: Two application-specific ENTRUST controllers
- ENTRUST_FX: An ENTRUST controller applied to a business-critical e-finance service-based system
- ENTRUST_UUV: An ENTRUST controller applied to a mission-critical embedded system from the unmanned vehicle domain
All directories (controller and examples) are Maven Eclipse projects.
--
Should you have any comments, suggestions or questions, please email us at simos-at-cs.york.ac.uk