Envisage Deliverables

This page contains the public deliverables of Envisage

The Case Studies

  • D4.2.1 Initial Modeling of the ATB Case Study. This deliverable reports on the initial modeling of the structural and functional aspects of the ATB case study and its informal requirements, and details how the case study plans to cover the objectives of Envisage.
  • D4.2.2 Resource-aware Modeling of the ATB Case Study. This deliverable presents a resource-aware model of the ATB Case Study: the ABS model of the structural
    and functional aspects of the ATB case study and its requirements. The emphasis is on mobile device modeling rather than crawling, to better reflect changes in the actual system we try to model.
  • D4.2.3 Assurance of the ATB Case Study. This deliverable reports on the Memkite case study and discusses different aspects of its modeling and analysis. The focus for the modeling phase includes bandwidth usage. The focus for analysis has been on tools for simulation, deadlock analysis, and systematic testing.
  • D4.3.1 Initial Modeling of the FRH Case Study. This deliverable reports on the initial modeling of the structural and functional aspects of the FRH case study and its informal requirements, and details how the case study plans to cover the objectives of Envisage.
  • D4.3.2 Resource-aware Modeling of the FRH Case Study. This deliverable reports on the modeling of the resource-aware version of the FRH case study and deployment scenarios in the abstract behavioral specification language, using the Envisage modeling techniques.
  • D4.3.3 Assurance of the FRH Case Study. This deliverable shows how the ABS language and its extensions (developed in WP1 and WP2) were able to successfully capture the Fredhopper Cloud Services. New material in D4.3.3 focuses on quality assurance for the FRH model through the application of the analysis techniques developed in WP3 as well as simulation, the modeling of FRH SLAs, dynamic deployment, monitoring and visualization.
  • D4.4.1 Initial Modeling of the ENG Case Study. This deliverable reports on the initial modeling of the structural and functional aspects of the ENG case study and its informal requirements, and details how the case study plans to cover the objectives of Envisage.
  • D4.4.2 Resource-aware Modeling of the ENG Case Study. This deliverable reports on the detailed modelling of the different deployment scenarios of the ENG case study in the abstract behavioural specification language.
  • D4.4.3 Assurance of the ENG Case Study. This deliverable reports on the results of applying the Envisage toolset to the ABS model developed for the case study. The specific tools applied were: Model Simulation (i.e., execution in the Erlang Backend for ABS); Deadlock Analysis; Resource Analysis (specifically w.r.t. computational cost); and Automatic Java Code Generation.
  • D4.5 Overall Assessment. This deliverable contains the overall assessment of the methodology, modeling artifacts, and tool-supported analysis techniques developed in Envisage. The assessment is in terms of the expected project outcomes, the initial user requirements, and the relation of the case studies to the project objectives.

Modeling & Simulation

  • D1.1 Modeling of Systems. This deliverable describes a modeling language for abstract behavioral specification which supports the executable modeling of distributed services in the context of architectural models of high-level deployment scenarios.
  • D1.2.1 Modeling of Resources (Initial Report). This deliverable formalizes virtualized resources and integrates them into the syntax and semantics of the object-oriented modeling language. We aim to introduce virtualized resources as first class citizens of the modeling language, and connect them to concepts of execution and locality.
  • D1.2.2 Modeling of Resources (Final Report). This deliverable describes the formalization of virtualized resources and their full integration into the syntax and semantics of the abstract behavioral specification language.
  • D1.3.1 Modeling of Deployment (Initial Report). Deployment can be seen as the problem of allocating to computing entities the resources they need to properly run. This deliverable reports on initial work on modeling deployment in ABS.
  • D1.3.2 Modeling of Deployment (Final Report). This deliverable describes the integration of deployment scenarios related to virtualization into ABS.
  • D1.4.1 Simulation Demonstrator 1. This deliverable is a prototype and description of the basic simulation engine which functions like a debugger for executable models, in which different execution strategies may be explored.
  • D1.4.2 Simulation Demonstrator 2. This deliverable is a prototype combining system level descriptions with resource and deployment models to allow rapid prototyping. The simulation environment closely reflects the formal semantics of the modeling language, yet allows the rapid prototyping of models in different deployment scenarios and with different load balancing strategies.

Service Contracts

Analysis & Automation

  • D3.1 Code Generation. This deliverable reports on the automatic generation of target code from ABS. The deliverable is a prototype and description of the code generation tool, targeting Java and Haskell.
  • D3.2 Verification. This deliverable reports on dynamic logic for ABS, on the development of the KeY-ABS tool for deductive verification, and the DF4ABS tool for deadlock detection.
  • D3.3.1 Resource Analysis. This deliverable consists of a tool prototype for an initial version of the planned automated resource analysis.
  • D3.3.2 Resource Analysis. This deliverable presents the main concepts and settings of the resource analyzer SACO, including a user manual.
  • D3.4 Hybrid Analysis. During Envisage a wide range of formal analyses for the ABS language have been realized, including deadlock detection, deductive verification, resource bound computation, test case generation, type systems. Many of these approaches only unfold their full impact in combination with each other, as well as in combination with the ABS simulation tool. In this report we describe a number of such hybrid approaches that were explored in Envisage. The results go beyond the state-of-art of what is possible in each individual method.
  • D3.5 Test Case Generation. This deliverable documents a prototype. The basic concepts for testing abstract behavioral models are xplained, including dynamic and static testing, and deadlock-guided testing. End user documentation is provided for two testing tools developed in the project:  SYCO, used for dynamic (optionally deadlock-guided) testing, and  aPET, used for static testing and test case generation by means of symbolic execution.

Management & Outreach