FREE ELECTRONIC LIBRARY - Books, abstracts, thesis

Pages:   || 2 | 3 |

«IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII IST-004527 ARTIST2 Network of Excellence on Embedded Systems Design ...»

-- [ Page 1 ] --

IST-004527 ARTIST2 NoE Year 4

Cluster: Testing and Verification D2-Mgt-Y4-VII

IST-004527 ARTIST2

Network of Excellence

on Embedded Systems Design

Cluster Progress Report for Year 4


Testing and Verification

Cluster Leader:

Director, Professor Kim Guldstrand Larsen

CISS, Aalborg University, Denmark


Policy Objective (abstract)

The objective is to combine the efforts and skills of the individual leading researchers and research groups in Europe into a world-class virtual team, for advancing the state-of-the-art in verification and testing methodologies. Meeting place Testing and verification is a transversal topic interacting with all the other topics in embedded systems design aiming to ensure that the different design steps meet given properties as well as the overall correctness of the implementation. Focus within the cluster is on two aspects being of extreme importance for embedded systems. First is the verification and testing of quantitative properties ensuring that real-time constraints and quality of service constraints are met. Second is the verification of security properties. A particular objective is the successful transfer of knowledge, methods and tools to industry.

1/20 IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII Table of Contents

1. Overview

1.1 High-Level Objectives

1.2 Industrial Sectors

1.3 Main Research Trends

2. State of the Integration in Europe

2.1 Brief State of the Art

2.2 Main Aims for Integration and Building Excellence through Artist2

2.3 Other Research Teams

2.4 Interaction of the Cluster with Other Communities

3. Overall Assessment and Vision for the Cluster

3.1 Assessment for Year 4

3.2 Overall Assesment since the start of the Artist2 NoE

3.3 Vision Beyond the Artist2 NoE

4. Cluster Participants

4.1 Core Partners

4.2 Affiliated Industrial Partners

4.3 Affiliated International Partners

5. Internal Reviewers for this Deliverable

–  –  –

1. Overview In this section we give an overview of the current situation for the cluster’s research area in terms of overall objectives and trends.

1.1 High-Level Objectives The high level objectives for the 18 months period, February 2007 until August 2008, are as


• Quantitative Testing and Verification: included continued effort towards efficient tool components for controller synthesis, initiation of work on property-preserving code generation, development of generic frameworks using abstraction and compositionality for efficient analysis of quantitative models and new debugging and analysis techniques based on various combinations of testing and verification techniques. lskdjfjjsflksjfskjf Also, based on existing powerful (real-time) verification techniques work towards maturing and further development of important topics such as optimal scheduling, monitoring and fault diagnosis, controller synthesis, robustness and implementability of quantitative models and analysis of hybrid models, stochastic and timed models has been planned.

• Testing and Verification Platform for Embedded Systems: Systems the objectives include continued improvement related to the individual tools, their advancement and dissemination as well as application on industrial case studies. Also, the objectives include a high performance tools server.

• Verification of Security Properties: Based on a decision made at the last review, the activities on security have been embedded within the two activities above.

For Quantitative Testing and Verification almost all objectives have been accomplished.

Substantial research advancing state-of-the-art of controller synthesis has been made covering synthesis with budget constraints, partial observability, modular and distributed synthesis, costoptimality, synthesis with respect to bounded response properties.

A variety of quantitative models have been introduced and throurougly examined, including models with resources (e.g. cost, energy, memory consumption, stack size, etc) as well as stochastic aspects. Methods supporting compositionality and component based development using rich interfaces (i.e. quantitative component specifications) have been provided and abstraction of quantitative models (both stochastic and hybrid) have provided the basis for efficient analysis methods.

Novel debugging and analysis techniques have been provided including techniques based on heuristic and guided search, off-line test generation using games as well as symbolic model checking techniques.

Robustness and implementability has been subject to less activity than anticipated. However, within upcoming newly started FP7 STREP projects these topics will be pursued during the next years.

Within Testing and Verification Platform for Embedded Systems all objectives have been accomplished. The individual tools have been further refined – both with respect to functionality and performance. E.g. The tool UPPAAL TIGA now offers a mature tool for (timeIST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII optimal) synthesis for timed games models with a growing number of industrial applications.

Also, the work of dissemination of the tools through case study demonstrators has been continued and documented through the joint web page for industrial case studies. Finally, the high performance tools server has been completed making the tools suitable for 64 bit architetures and distributed PC clusters available via a common web interface.

1.2 Industrial Sectors The testing and verification techniques and tools developed and disseminated within the cluster have relevance and potential impact on literally all industrial sectors developing or using embedded systems solutions. Within the Strategic Research Agenda of the ARTEMIS research platform1 Design Methods and Tools is one of the three research priorities put forward. Here model- and component-based approaches are proposed as necessary for coping with the growing complexity of systems while meeting “time-to-market” requirements.

Methods and tools for testing and verification are to play a central role in the ARTEMIS

research strategy, as can be seen from the following citations:

• “.. methods and tools for simulation, automatic validation and proving, and virtual Verification and Validation (V&V). Methods and tools for developing product lines of embedded systems.” • “.. reduce the cost of the system design by 50%. Matured product family technologies will enable a much higher degree of strategic reuse of all artifacts, while component technology will permit predictable assembly of Embedded Systems.” • “.. achieve 50% reduction in development cycles. Design excellence will aim to reach a goal of “right first time, every time” by 2016, including Validation, Verification and certification (to the same and higher standards as today).” • “..manage a complexity increase of 100% with 20% effort reduction. The capability to manage uncertainty in the design process and to maintain independent hardware and software upgradeability all along the life cycle will be crucial.” • “.. reduce by 50% the effort and time required for re-validation and recertification after change, so that they are linearly related to the changes in functionality.” The industrial needs for improved tools and methods for system validation have also been witnessed by a number of industrial and industry inspired case-studies and projects using model-based testing and verification carried out by the individual partners. Detailed information of these (and others) is to be found in the ARTIST2 Open Repository for Test and

Verification Case Studies (https://bugsy.grid.aau.dk/artist2), and include:

• Danfoss (Aalborg): The project has two main goals. One is to develop an automated test execution environment for system level testing of the EKC series refrigeration controllers. The other is to improve model-based online testing given the experiences from the first trials

• ESI (Embedded Systems Institute, Eindhoven) has carried out (is carrying out) large industrial case studies with Océ, ASML, Philips Semiconductors (now NXP), Philips Medical Systems, Vanderlande Industries.

• Ericsson Telebit (Aalborg): The goal of this project has been to use Live Sequence Charts in a model-driven approach to the testing of TCP/IP internet protocols. Live Sequence Charts are used to capture (informal) RFC in a formal, yet intuitive, way.


–  –  –

• Novo Nordisk A/S. (Aalborg) Automaic generation of test cases from UML statechart models of MMI (man machine interface) for medical devices. Each statechart model describe a specific class of usage scenarios, and test cases are derive in two steps.

First the model is translated into an equivalent timed automata. Then the automata is analysed based on various parameters (coverage criteria, search depth, etc) reslting in a number of test cases expressed in the company specific scripting language. The obtained coverage and possibly unreachable states are reported.

• OFFIS, University of Freiburg, Aalborg University: The "Single-tracked Line Segment" (SLS) case study stems from an industrial partner of the UniForM-project. It is the specification of a control system for a single-tracked line segment for tramways. It is implemented by distributed PLC automata. We took three different models of the SLS case study as examples. As the safety property to verify, we chose the mutual exclusion of drive permissions, i.e., the control system never gives permission to both directions simultaneously.

• OFFIS; Univ. of Oldenburg; Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik: The flap controller (high-lift) case study is derived from a case study for Airbus, a controller for the flaps of an aircraft. The flaps are extended during take-off and landing to generate more lift at low velocity. They are not robust enough for high velocity, so they must be retracted for other periods. The controller can perform a loadrelief function to correct the pilot's commands if he endangers the flaps. Additionally, there is also an extensive monitoring of the health of its sub-systems, checking for instance for hardware failures. Typically this will give rise to large discrete state spaces when model checking models derived from the flap controller.

• OFFIS, Univ. of Oldenburg : Automating verification of cooperation, control, and design in traffic applications. Here we present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.

• Scott/Tiger Validate (Aalborg): From timed automata design models the verification engine of UPPAAL is used for off-line generation of test-sequences which covers the model. In the project a tool for translating these logical test-sequences to test-scripts executable in, e.g., QTP of Mercury’s Test Director. The resulting tool-chain has been applied to automatic testing of web-services of TDC (Danish Telecom). A commercial spin-off tool (V+) has been developed.

• Skov A/S (Aalborg): In this work, we provide a complete tool chain for automatic controller synthesis using UPPAAL Tiga and Simulink. The tool chain is explored using an industrial case study for climate control in a pig stable. The problem is modelled as a game, and UPPAAL Tiga is used to automatically synthesize a safe strategy that is transformed for input to Simulink, ´which is used to run simulations on the controller and generate code that can be executed in the actual pig stable. The models allow for guiding the synthesis process and generate different strategies that are compared through simulations.

• Dependable Systems and Software (DSS) group at Saarland university, Formal Methods and Tools group (FMT) and Design and Analysis of Communication Systems 5/20 IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII (DACS) group at the university of Twente: Arcade models. These include two case studies found in the literature, namely a Distributed Database Architecture and a Reactor Cooling System. Arcade tool was used which is based on the input/output interactive Markov chains formalism.

• DSS group at Saarland university, FMT and DACS groups at the university of Twente:

Dynamic Fault Tree (DFT) models These include four case studies that also appeared in the literature, namely the cascaded PAND system, the cardiac assist system, the multi-processor distributed computing system, and the fault-tolerant parallel processor.

Coral tool was used which is based on the input/output interactive Markov chains formalism.

• Software engineering group and FMT group at the university of Twente: Open-source Media Player. This case study was conducted on a publicly available open-source media player called MPlayer (http://www.mplayerhq.hu/). We have modeled the recovery mechanism implemented for the MPlayer and analyzed the availability of the system. Few tools were used including the FLORA framework and the CADP tool set (http://www.inrialpes.fr/vasy/cadp/). The input/output interactive Markov chains formalism was used.

Pages:   || 2 | 3 |

Similar works:

«Journal of Information, Information Technology, and Organizations Volume 4, 2009 Communication and Culture in Global Software Development: The Case of Mauritius and South Africa Maureen Tanner University of Cape Town, Cape Town, South Africa M.Tanner@uct.ac.za Abstract Global Software Development (GSD) is a growing sector in Mauritius and South Africa. With an increasing number of information technology (IT) investors, both countries are being recognised as IT hubs in the Southern African...»

«Evaluation of Groundwater Resources of West Amwell Township, Hunterdon County, New Jersey M2 Associates Inc. 56 Country Acres Drive Hampton, New Jersey 08827 EVALUATION OF GROUNDWATER RESOURCES OF WEST AMWELL TOWNSHIP, HUNTERDON COUNTY, NEW JERSEY FEBRUARY 14, 2003 Prepared for: Township of West Amwell Hunterdon County 150 Rocktown-Lambertville Road Lambertville, New Jersey 08530-3203 Prepared by: Matthew J. Mulhall, P.G. M2 Associates Inc. 56 Country Acres Drive Hampton, New Jersey 08827-4110...»

«Voting to Tell Others∗ Stefano DellaVigna John A. List Ulrike Malmendier UC Berkeley and NBER U Chicago and NBER UC Berkeley and NBER Gautam Rao UC Berkeley This version: February 27, 2013 Abstract Why do people vote? We argue that signaling utility plays a significant role in explaining voting behavior: people vote because others might ask. We construct a model in which individuals may derive pride from signaling to others that they voted and, conversely, feel shame or guilt from admitting...»

«This document is scheduled to be published in the Federal Register on 12/23/2015 and available online at http://federalregister.gov/a/2015-32145, and on FDsys.gov [4830-01-p] DEPARTMENT OF THE TREASURY Internal Revenue Service 26 CFR Part 1 [REG-109822-15] RIN 1545-BM70 Country-by-Country Reporting AGENCY: Internal Revenue Service (IRS), Treasury. ACTION: Notice of proposed rulemaking. SUMMARY: This document contains proposed regulations that would require annual country-by-country reporting by...»

«Turkish Online Journal of Distance Education-TOJDE July 2006 ISSN 1302-6488 Volume: 7 Number: 3 Article: 8 Developing Web-oriented Homework System to Assess Students’ Introductory Physics Course Performance and Compare to Paper-based Peer Homework Neset DEMIRCI Balıkesir University Necatibey Faculty of Education Department of Physics Education Balikesir, TURKEY ABSTRACT The World Wide Web influences education and our lives in many ways. Nowadays, Web-based homework has been becoming...»

«Winter 2013 Postdoctoral Fellowship Awards will activate on July 1, 2013. Funding components offering this program and deadline dates are as follows: • Founders Affiliate Jan. 22, 2013 • Midwest Affiliate Jan. 28, 2013 • Great Rivers Affiliate – Jan. 23, 2013 • SouthWest Affiliate – Jan. 29, 2013 • Greater Southeast Affiliate Jan. 23, • Western States Affiliate – Jan. 29, • Mid-Atlantic Affiliate – Jan. 22, 2013 Program Description, Eligibility and Peer Review Criteria...»

«McMillan, Amy Jenefer (2013) What is special about family relationships? Familial attributions and emotional responses to relatives who present with challenging behaviour & Clinical research portfolio. D Clin Psy thesis. http://theses.gla.ac.uk/4155/ Copyright and moral rights for this thesis are retained by the author A copy can be downloaded for personal non-commercial research or study, without prior permission or charge This thesis cannot be reproduced or quoted extensively from without...»

«Payments and Reimbursements Foreign Non-Affiliates Global Support Services 4/21/2015 Table of Contents Definitions Understanding Restrictions Determining Immigration and Work Authorization Status Inviting a Foreign National Guest Types of Payments Payment Process Honorarium Payment Travel Payments and Reimbursements Independent Contractor and Consultant Fee Payment Payment Method and Timeline Payment Points to Consider APPENDIX Contacts and Responsibilities Sample Scenarios Conference...»

«EUROPEAN COMMISSION Brussels, 9.9.2015 COM(2015) 453 final COMMUNICATION FROM THE COMMISSION TO THE EUROPEAN PARLIAMENT AND TO THE COUNCIL EU Action Plan on return EN EN I. Introduction Return of irregular migrants who do not have a right to stay in the EU to their home countries, in full respect of the principle of non-refoulement, is an essential part of EU's comprehensive efforts to address migration and in particular to reduce irregular migration. The European Agenda on Migration1, adopted...»

«i ABSTRACT The SABC has embraced a mandate that advocates the promotion of cultural diversity within the broader ambit of national identity. Although SABC3 consitutes the commercial wing of the station, it too is required to produce programmes in accordance with the spirit of this mandate. With tight budgets, pressure for audience ratings and an assortment of individual producers with individual production agendas, it may be naïve to presume that the SABC could consistently give priority to...»

«DEEP REACTIVE BARRIERS FOR REMEDIATION OF VOCs AND HEAVY METALS Grant Hocking, Samuel L. Wells and Rafael I. Ospina GeoSierra LLC, Atlanta, GA, USA. ABSTRACT: Azimuth controlled vertical hydraulic fracturing technology has constructed full scale in situ iron reactive permeable barriers at moderate to significant depth for remediation of groundwater contaminated with chlorinated hydrocarbons and metals. Zero valent iron reactive permeable barriers have been installed to remediate chlorinated...»

«Oxford Futures Forum Abstracts (version 2) 1. Aliakseyeu, Dzmitry 2. Barchan, Margareta 3. Bason, Christian 4. Bock, Ute 5. Boradkar, Prasad 6. Brassett, Jamie 7. Candy, Stuart 8. Chermack, Tom 9. Chraibi, Sanae 10. Collyns, Napier 11. Crook, Paul 12. de Ruijter, Paul 13. DiPaola, Paul 14. Drenth, Gerard 15. Dunagan, Jake 16. Eden, Grace 17. Eidinow, Esther 18. Elahi, Shirin 19. Flinn, Joanne 20. Forlano, Laura 21. Fuller, Ted 22. Gano, Gretchen 23. Gatti, Luca 24. Gentzel, Todd 25. Grönquist,...»

<<  HOME   |    CONTACTS
2016 www.book.xlibx.info - Free e-library - Books, abstracts, thesis

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.