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
- D2.1 Behavioral Interfaces for Virtualized Services. This deliverable reports on the definition of behavioral interfaces for services and their formal relationship. The deliverable also addresses the problem of interoperability obligations that can be enforced with behavioral interfaces.
- D2.2.1 Formalization of Service Contracts and SLAs (Initial Report). This deliverable reports on initial work on a formal language for modeling SLA documents and on extending behavioral interfaces with quality of services descriptions that address virtualized resources and deployment models.
- D2.2.2 Formalization of Service Contracts and SLAs (Final Report). This deliverable reports on work to bridge the gap between (parts of) SLAs and services by (i) developing a formal language for modelling SLA documents, (ii) providing behavioural interfaces with quality of services descriptions that address virtualised resources and deployment models and (iii) defining techniques to assess the compatibility between SLAs and service contracts.
- D2.3.1 Monitoring Add-Ons and Visualization (Initial Report). We define a layered declarative model to capture user-level SLAs, low-level metrics and billable events, and relate this model to ABS and its analysis tools.
- D2.3.2 Monitoring Add-Ons and Visualization (Final Report). This deliverable documents a prototype event-based, service-oriented monitoring and visualization framework for observing the performance and detecting the failures of services.
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
- D5.2.1 Envisage Collaboratory (Initial Version). This deliverable is a prototype documenting the initial version of the Envisage Virtual Collaboratory.
- D5.2.2 Envisage Collaboratory (Final Version). The Virtual Collaboratory of Envisage aims at making tools and technologies developed in the context of Envisage available for the general public as online services. This report supplements the prototype by documenting background work to realize the collaboratory.
- D5.3 Envisage Work Flow. This deliverable reports on how Envisage technologies may be used in software development processes by suggesting work flows for using the ABS modeling language and associated tools. Two different and complementary work flows are discussed in the deliverable and related to existing software development processes.
- D5.4.3 Final Report on Academic Reach-Out. This deliverable is a report on the organization of two workshops related to Envisage.
- D5.5.3 Final Report on Industrial Reach-Out. This deliverable reports on industry and community dissemination efforts throughout the entire Envisage project.
- D5.6 Market Analysis & Initial Exploitation Plan. This deliverable reports on preliminary results of the market analysis and exploitation activities, and describes exploitable items based on Envisage outcomes.
- D5.7 Business Strategy & Revised Exploitation Plan. This deliverable focuses on business strategy in the context of Envisage.
- D6.2: Web Site and Project Presentation. This deliverable documents the Envisage website and the material for project presentation.