Model checking

Model checking

Con el nombre Model checking se conoce a un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe satisfacer una especificación formal descrita mediante una fórmula, a menudo escrita en alguna variedad de lógica temporal.

El modelo suele estar expresado como un sistema de transiciones, es decir, un grafo dirigido, que consta de un conjunto de vértices y arcos. Un conjunto de proposiciones atómicas se asocia a cada nodo. Así pues, los nodos representan los estados posibles de un sistema, los arcos posibles evoluciones del mismo, mediante ejecuciones permitidas, que alteran el estado, mientras que las proposiciones representan las propiedades básicas que se satisfacen en cada punto de la ejecución.

Formalmente, el problema se representa de la siguiente manera: Dada una propiedad deseada, expresada como una fórmula en lógica temporal p, y un modelo M con un estado inicial s; decidir si M,s \models p.

Existen herramientas automáticas para realizar el Model checking, basadas en técnicas combinatorias, explorando el espacio de estados posibles; lo que conduce al problema de explosión de estados. Para evitarlo, diversos investigadores han desarrollado técnicas basadas en algoritmos simbólicos, abstracción, reducción de orden parcial y model checking al vuelo. Inicialmente, las herramientas se diseñaron para trabajar con sistemas discretos, pero han sido extendidas a sistemas de tiempo real, o sistemas híbridos.

Los inventores del método, Edmund M. Clarke, E. Allen Emerson y Joseph Sifakis, recibieron el Premio Turing 2007 de la ACM, en reconocimiento de su fundamental contribución al campo de las ciencias de la computación.

Enlaces externos


Wikimedia foundation. 2010.

Игры ⚽ Поможем написать реферат

Mira otros diccionarios:

  • Model Checking — (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für eine gegebene… …   Deutsch Wikipedia

  • Model Checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Model checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking (disambiguation) — Model checking may refer to model checking regression model validation This disambiguation page lists articles associated with the same title. If an internal link led you here, you may wish to chan …   Wikipedia

  • Abstraction model checking — is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down abstract version.The set of variables are partitioned into visible and invisible depending… …   Wikipedia

  • Model-based testing — is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test (SUT), or to represent the desired… …   Wikipedia

  • Model audit — A model audit is the colloquial term for the tasks performed when conducting due diligence on a financial model, in order to eliminate spreadsheet error. (Also known as Model Review in some areas). A study in 1998 concluded that even MBA students …   Wikipedia

  • Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… …   Wikipedia

  • Model View ViewModel — The Model View ViewModel (MVVM) is an architectural pattern used in software engineering that originated from Microsoft as a specialization of the Presentation Model design pattern introduced by Martin Fowler.[1] Largely based on the Model view… …   Wikipedia

Compartir el artículo y extractos

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