نویسندگان
دانشکده فنی و مهندسی - گروه کامپیوتر - دانشگاه تربیت مدرس
چکیده
کلیدواژهها
عنوان مقاله [English]
نویسندگان [English]
Dynamic Verification, dealing with the validation of the run-time behavior of software, faces the challenges of constructing a run-time behavior verifier and a mapping between behavior and environmental events. In this paper, we\ propose\ an approach,\ based\ on\ the Event\ Calculus \ called\ EBV,\ that presents an automatic approach to the challenges by taking four steps. In the first step, using the Parnas model, we document the requirements, including interaction between the environment and the software and, in the second step, we present a high-level and event-based specification of the expected behavior of the software in response to environmental events. In the third step, we extract a middle-level and state-based specification from the event-based one (the first mapping). The specification is a reference point for verifying the correct and expected behaviors. In the fourth step, by exploiting the State Design pattern, we implement the verifier, using the mapping of the state-based specification on run-time activities of the software (the second mapping). In this way, i.e. by two mappings, we provide the connection between the high-level environmental events and the low-level run-time activities of the software. In an attempt to show the effectiveness of the EBV, we construct the verifier of a safety-critical software from its specifications and pursue it to its implementation.
کلیدواژهها [English]
--
)