DOC PREVIEW
Integrated Functional and Non-Functional Design Verification for Embedded Software Systems

This preview shows page 1-2-3-4 out of 12 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Paper Number 09AE-0202 Integrated Functional and Non-Functional Design Verification for Embedded Software Systems Christopher Ackermann, Arnab Ray Fraunhofer Center for Experimental Software Engineering Rance Cleaveland Dept. of Computer Science, University of Maryland Charles Shelton, Chris Martin Robert Bosch North America, Research and Technology Center Copyright © 2008 SAE InternationalABSTRACT This paper describes an approach to integrating functional and non-functional design verification for embedded control software. The method uses functional models, which have traditionally been used in functional verification processes, to drive non-functional verification also. This is achieved by defining strategies for extracting non-functional models, which contain structural and quantitative information about non-functional characteristics such as performance and modifiability, from functional ones. Non-functional verification tools may then be used on the resulting models to check that desired non-functional properties, such as ease of modification, are catered for in the design. An extended example involving the analysis of a model for modifiability is presented, as is tool support for extracting non-functional models from functional ones. INTRODUCTION An emerging best-practice in embedded-software engineering is to conduct extensive verification and validation (V&V) during the design phases of the development process, in order to catch errors and inconsistencies as early as possible. The widespread adoption of model-based development within the automotive industry has opened up broad new opportunities for design V&V, since the availability of executable models in notations like Simulink® / Stateflow®1 and ASCET®2 at design time enables extensive testing and analysis to be undertaken before any source code has actually been written. In conventional model-based development workflows, design models are first constructed and then verified against the functional requirements (specifications of what the system must or must not do) using simulation, coverage-based testing, or model-checking. Requirements that relate to the non-functional aspects of system behavior (for instance resource usage, timeliness, modifiability) are typically reasoned about, if at all, in an ad-hoc qualitative manner. The motivation for the work in this paper is to give embedded software designers tools to conduct rigorous, coordinated non-functional and functional design verification and validation. The proposed approach to achieving this goal relies on the use of functional models in notations such as Simulink to drive both functional and non-functional design analysis, using tools developed in the Computer Science research community to undertake 1 MATLAB®, Simulink® and Stateflow® are registered trademarks of The MathWorks, Inc. 2 ASCET® is a registered trademark of ETAS GmbH.the latter. The core technical contribution described in this paper is an automated framework, and associated tools, for extracting non-functional design models from functional ones, so that appropriate verification of non-functional properties may be done at design time. The rest of the paper is arranged as follows. The next section provides background in functional and non-functional modeling and verification, with a focus on the specific non-functional attribute of modifiability. Strategies for computing modifiability models from functional ones are explained, and an example and tooling described. The paper then concludes. FUNCTIONAL AND NON-FUNCTIONAL MODELING AND VERIFICATION This section briefly reviews functional modeling and verification and introduces the approach to non-functional modeling and verification that is used in this paper. FUNCTIONAL VERIFICATION A functional model of a system is a mathematical specification of the operational behavior of the system. It is typically encoded using an executable modeling notation. A functional requirement is a statement of what the system must or must not do, usually expressed in the form: if a given condition holds, then the system should respond appropriately. Functional verification consists of checking whether the functional model satisfies the functional requirements. Simulink is widely used in the automotive industry for functional modeling. In Simulink, a model consists of a number of blocks (units of functionality) that exchange typed data (signals) through what are known as connections. These blocks are hierarchical; a block, in turn, may consist of other blocks and inter-connections between them. Blocks that contain other blocks are typically referred to as subsystems. In Figure 1, a Simulink diagram is shown of an abstracted body control application function. The top subsystem (X) handles all high level inputs and provides all outputs of the diagram. X processes the input signals and controls the subsystems Y and Z accordingly. Both Y and Z report on their current state by feeding back a signal to X. Figure 1: Example functional model given in Simulink. Functional verification of models can be performed in a variety of ways: through exhaustive, guided simulation [1]; testing of the code automatically generated from the model [2];formal methods-based model checking or deductive reasoning [3]; and instrumentation-based model testing [4]. NON-FUNCTIONAL VERIFICATION While functional modeling and verification has been studied extensively and is becoming widespread in practice, comparatively little attention has been placed on formally checking designs against non-functional requirements. Such requirements typically refer to desired structural or system-related properties, such as performance (will the software ensure desired timing?), security (does the software preclude unintended use?) and modifiability (is the software easy to modify and extend?). In the Computer-Science research community, technologies such as ArchE [5] have been developed for reasoning rigorously about the non-functional aspects of software designs. ArchE focuses on software-architecture models as the design artifacts of interest; it allows designers to build such models and analyze them for different non-functional properties. In ArchE, basic software architecture information is enriched with quantitative information regarding the non-functional aspect of interest (modifiability, performance, etc.).


Integrated Functional and Non-Functional Design Verification for Embedded Software Systems

Download Integrated Functional and Non-Functional Design Verification for Embedded Software Systems
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Integrated Functional and Non-Functional Design Verification for Embedded Software Systems and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Integrated Functional and Non-Functional Design Verification for Embedded Software Systems 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?