Real-Time Systems. Design Principles for Distributed Embedded Applications. Herman Kopetz. Second Edition (811374), страница 86
Текст из файла (страница 86)
HOW to choose the test cases? There are different options to choose the testcases: random, guided by the operational profile, looking at a specific demand onthe system (e.g., a shut down scenario of a nuclear reactor), or based onknowledge about the internal structure of the program (see Sect.
12.2.2).3. HOW MUCH testing is sufficient? The decision about how many test casesmust be executed can be derived from coverage analysis or from reliabilityconsiderations.4. WHAT is it that we execute? What is the system under test – a module, thesystem in a simulated environment or the system in its real-world target environment?5. WHERE do we perform the observation? This depends on the structure of thesystem and the possibility to observe the behavior of subsystems withoutdisturbing the system operation.6. WHEN is it in the product lifecycle that we perform the test? In the early phases ofthe lifecycle, testing can only be performed in an artificial laboratory environment.
The real test comes when the system is exercised in its target environment.12.3Testing of Component-Based SystemsThe component-based design of embedded applications, which is the focus of thisbook, requires appropriate strategies for the validation of component-based systems.A component is a hardware/software unit that encapsulates and hides its design andmakes its services available at the message-based LIF (linking interface) of thecomponent. While the component provider has knowledge about the internals of acomponent and can use this knowledge to arrive at effective test cases, the component user sees a component as a black box and must use and test the component onthe basis of the given interface specification.12.3.1 Component ProviderA component provider sees a component independent from the context of use.The provider must be concerned with the correct operation of the component in allpossible user scenarios.
In our component model, the user scenarios can be parameterized via the Technology Independent Interface (TII, see Sect. 4.4.3). Thecomponent provider must test the proper functioning of the component in the full29812 Validationparameter space supported by the TII. The component provider has access to thesource code and can monitor the internal execution within the component acrossthe Technology Dependent Interface (see Sect. 4.4.4), which is normally not utilizedby the component user.12.3.2 Component UserThe component user is concerned with the performance of the component in itsconcrete context of use that is defined by a concrete parameter setting of thecomponent for the given application.
The component user can assume that theprovider has tested the functions of the component as specified by the interfacemodel and will put the focus of testing on the effects of component integration andthe emerging behavior of a set of components, which is outside the scope of testingof the component provider.In a first step, a component user must validate that the prior properties of thecomponent, i.e., the properties that the component supplier has tested in isolation,are not refuted by the integration of the component. The component integrationframework plays an important role in this phase.In an event-triggered system, queues must be provided at the entry and exit of acomponent to align the component performance with the pending user requests, withthe user’s capability to absorb the results in a timely manner and with the transportcapabilities of the communication system.
Since every queue has a potential foroverflow, flow-control mechanisms are needed across component boundaries. In thetest phase the reaction of the component to queue overflow must be examined.The integration of components can give rise to planned or unanticipated emergent behavior that is caused by the component interactions. Emergent behavior isthat which cannot be predicted through analysis at any level simpler than that of thesystem as a whole [Dys98, p. 9]. This definition of emergent behavior makes it clearthat the detection and handling of emergent behavior is in the realm of a componentuser and not of the component supplier.
Mogul [Mog06] lists many examples ofemergent behavior in computer systems that are caused by the interaction ofcomponents. The appearance of emergent behavior is not well-understood and asubject of current research (see also Sect. 2.4).12.3.3 Communicating ComponentsDuring system integration, commercial-off-the-shelf (COTS) components orapplication-specific components are connected by their corresponding linkinginterfaces (LIFs). The message-exchange across these linking interfaces must becarefully tested.
In Sect. 4.6 we have introduced three levels of a LIF specification:the transport level, the operational level and the semantic level. The LIF tests canfollow along these three levels. The test at the transport level and the operational12.4 Formal Methods299level, which must be precisely specified, can be performed mechanically, while thetest of the meta-level (the semantics) will normally need human intervention. Themulti-cast capability of the BMTS (basic message transport service) – see Sect. 6.1)enables the probe-effect-free observation of the information exchanged amongcommunicating components.In model-based design (Sect. 11.3.1), executable models of the behavior of thephysical plant and of the control algorithms for the computer system are developedin parallel.
At the PIM level these models, embodied in components, can be linkedin a simulation environment such that the interaction of these components can beobserved and studied. In a control system, the performance (quality of control) ofthe closed loop system can be monitored and used to find the optimal controlparameter setting. The simulation will normally operate on a different time-scalethan the target system. In order to improve the faithfulness of the simulation withrespect to the target system, the phase relationships of the messages exchangedbetween the PIM components of the plant and of the controller should be the sameas the phase relationships in the final implementation, the PSM.
This constant phaserelationship will avoid many subtle design errors caused by an uncontrolled andunintended phase relationship among messages [Per10].12.4Formal MethodsBy the term formal methods we mean the use of mathematical and logical techniques to express, investigate, and analyze the specification, design, documentation,and behavior of computer hardware and software. In highly ambitious projects,formal methods are applied to prove formally that a piece of software implementsthe specification correctly. John Rushby [Rus93, p. 87] summarizes the benefits offormal methods as follows:Formal methods can provide important evidence for consideration in certification, but theycan no more “prove” that an artifact of significant logical complexity is fit for its purposethan a finite-element calculation can “prove” that a wing span will do its job.
Certificationmust consider multiple sources of evidence, and ultimately rests on informed engineeringjudgment and experience.12.4.1 Formal Methods in the Real WorldAny formal investigation of a real-world phenomenon requires the following stepsto be taken:1.
Conceptual model building. This important informal first step leads to a precisenatural language representation of the real-world phenomenon that is the subjectof investigation.2. Model formalization. In this second step, the natural language representation ofthe problem is transformed, and expressed in a formal specification language30012 Validationwith precise syntax and semantics. All assumptions, omissions, or misconceptions that are introduced in this step will remain in the model, and limit thevalidity of the conclusions derived from the model. Different degrees of rigorcan be distinguished.3. Analysis of the formal model.
In the third step, the problem is formally analyzed.In computer systems, the analysis methods are based on discrete mathematicsand logic. In other engineering disciplines, the analysis methods are based ondifferent branches of mathematics, e.g., the use of differential equations toanalyze a control problem.4. Interpretation of the results. In the final step, the results of the analysis must beinterpreted and applied to the real world.Only step (3) out of these four steps can be fully mechanized. Steps (1), (2), and (4)will always require human involvement and human intuition and are thus as fallibleas any other human activity.An ideal and complete verification environment takes the specification,expressed in a formally defined specification language, the implementation, writtenin a formally defined implementation language, and the parameters of the executionenvironment as inputs, and establishes mechanically the consistency between specification and implementation.
In a second step, it must be ensured that all assumptions and architectural mechanisms of the target machine (e.g., the properties andtiming of the instruction set of the hardware) are consistent with the model ofcomputation that is defined by the implementation language. Finally, the correctness of the verification environment itself must be established.12.4.2 Classification of Formal MethodsRushby [Rus93] classifies the use of formal methods in computer science accordingto the increasing rigor into the following three levels:1. Use of concepts and notation of discrete mathematics. At this level, the sometimes ambiguous natural language statements about requirements and specification of a system are replaced by the symbols and conventions of discretemathematics and logic, e.g., set theory, relations, and functions.
The reasoningabout the completeness and consistency of the specification follows a semiformal manual style, as it is performed in many branches of mathematics.2. Use of formalized specification languages with some mechanical support tools.At this level, a formal specification language with a fixed syntax is introducedthat allows the mechanical analysis of some properties of the problemsexpressed in the specification language.
At level (2), it is not possible to generatecomplete proofs mechanically.3. Use of fully formalized specification languages with comprehensive supportenvironments, including mechanized theorem proving or proof checking.12.4 Formal Methods301At this level, a precisely defined specification language with a direct interpretation in logic is supplied, and a set of support tools is provided to allow themechanical analysis of specifications expressed in the formal specificationlanguage.12.4.3 Benefits of Formal MethodsLevel (1) methods.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
