Runtime verification

Runtime verification

Runtime verification is a verification technique that combines formal verification and program execution.It is the process of detecting faults in a system under scrutiny by passively observing its input/output behavior during its normal operations. The observed behavior, e.g., in terms of log traces, of the target system can be monitored and verified dynamically to satisfy given requirements. Such requirements are typically specified by a formalism which can express temporal constraints, such as LTL-formulae (Linear temporal logic) or automata and statecharts. In contrast to the classical model checking approach, where a simplified model of the target system is verified, runtime verification is performed while the real system is running. Thus, runtime verification or as it is sometimes referred to, passive testing, increases the confidence on whether the implementation conforms to its specification. Furthermore, it allows a running system to reflect on its own behavior in order to detect its own deviation from the prespecified behavior.

In contrast to other formal verification methods such as model checking, runtime verification has to deal with finite traces only, as at an arbitrary point in time the system will be stopped and so its execution trace. The exception to this rule is a deployed runtime monitor that monitors on a potentially never ending deployed application for the purpose of detecting requirement violations while the application is running. To this end the formal specification must contain a recovery specification.

Continuous monitoring of the runtime behavior of a system can improve our confidence in the system by ensuring that the current execution is consistent with its requirements at runtime. In the literature, at least the following four reasons are mentioned in order to argue for runtime verification:

* If you check the model of your system you cannot be confident on the implementation since correctness of the model does not imply correctness of the implementation.

* Some information is available only at runtime or is convenient to be checked at runtime.

* Behavior may depend heavily on the environment of the target system; then it is not possible to obtain the information necessary to test the system.

* In the case of systems where security is important or in the case of critical systems, it is useful also to monitor behavior or properties that have been statically proved or tested.

Another good reason to use runtime verification is that it allows for formal specification and verification or testing of theproperties that a system has imperatively to satisfy. Traditional testing techniques such as unit testing are ad hoc and informal. It is only a partial proof of correctness in that it does not guarantee that the system will operate as expectedunder untested inputs. In terms of its ability to guarantee software correctness, runtime verification is weaker than
formal methods but stronger than testing. Testing can only guarantee the correctness of a limited set of inputs at implementation time. As a result, undiscovered faults may result in failures at runtime, and even allowing the system to propagate corrupted output because the failure was not detected. By always monitoring the software for correctness, such failures can be caught when they happen, for any input which causes them to occur. However, runtime verification is weaker than formal methods because such guarantees can not be made a priori.

ee also

Research groups

* [http://runtime.in.tum.de/ Runtime Reflection at the Technical University of Munich]
* [http://eis.jpl.nasa.gov/lars/ NASA/JPL Laboratory for Reliable Software]
* [http://www.aspectbench.org/ AspectBench Compiler group] The AspectBench Compiler supports [http://abc.comlab.ox.ac.uk/papers#oopsla2005 tracematches] , a way to match on the execution history of Java and AspectJ programs.

Workshops

* [http://www.runtime-verification.org/ Workshops on Runtime Verification]
* [http://www.csd.uwo.ca/woda2005/ Workshop on Dynamic Analysis 2005]
* [http://www.dagstuhl.de/en/program/calendar/semhp/?semid=32256 2007 Dagstuhl Seminar on Runtime Verification]

Commercial

* [http://www.time-rover.com/ Time Rover, Inc]

References

* "Model-Based Testing of Reactive Systems", Broy, M. and Jonsson, B. and Katoen, J.-P. and Leucker, M. and Pretschner, A., Springer Press, 2005.

* The Humble Programmer, Edsger W. Dijkstra, CACM, October 1972

* "MODELING AND VERIFICATION USING UML STATECHARTS", Drusinsky, D., Elsevier, 2006, http://www.elsevier.com/wps/find/bookdescription.cws_home/707940/description#description


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Verification — The word Verify And Verification can refer to:* Verification and Validation: In engineering or a quality management system, verification is the act of reviewing, inspecting, testing, etc. to establish and document that a product, service, or… …   Wikipedia

  • Device driver synthesis and verification — The device driver is a program which allows the software or higher level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these …   Wikipedia

  • Java performance — Programs written in Java have had a reputation for being slower and requiring more memory than those written in natively compiled languages such as C or C++ (see e.g. [cite web url=http://www.jelovic.com/articles/why java is slow.htm title=Why… …   Wikipedia

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Design marker — In software engineering, a design marker is a technique of documenting design choices in source code using the Marker Interface pattern. Marker interfaces have traditionally been limited to those interfaces intended for explicit, runtime… …   Wikipedia

  • Java Virtual Machine — A Java Virtual Machine (JVM) is a set of computer software programs and data structures which use a virtual machine model for the execution of other computer programs and scripts. The model used by a JVM accepts a form of computer intermediate… …   Wikipedia

  • Exception handling — is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution. Programming languages differ considerably in their support… …   Wikipedia

  • Architecture .NET — Microsoft .NET Pour les articles homonymes, voir .Net. Microsoft .NET Déve …   Wikipédia en Français

  • DotNET — Microsoft .NET Pour les articles homonymes, voir .Net. Microsoft .NET Déve …   Wikipédia en Français

  • DotNet — Microsoft .NET Pour les articles homonymes, voir .Net. Microsoft .NET Déve …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”