Introduction to Formal Methods

 Abstract

Formal verification has been very useful in highly critical computer systems, ranging from air traffic systems to microcircuit design. When we talk about verification techniques of symbolic models of linear temporal logic (LTL), we must take into account that this technique helps us to represent in a natural way and by means of human logic, the correct development of processes that seem complex, but that through the use of mathematical symbologies, we can express in an understandable way.

Key words: Linear temporal logic (LTL), Formal methods.

Context

According to AF Domínguez (2018), temporal logic (TL, Temporal Logic) is a variant of modal logic that has as its focus the succession of events over time (Markey 2015). It extends propositional logic with modal and temporal operators such as: never, always, sometimes, sometimes, eventually, among others.

TL allows specifying qualitative properties (Konur 2013) -using standard TL- or quantitative properties -using TL with timed extensions- of the dynamic knowledge of a system to represent desirable behaviors. It even allows reasoning about how such behaviors change over time.

The standard TL expresses restrictions on the relative order of events or cases (for example:, in the expression "Every time (1) a customer requests to reserve an entity, (2) an employee must check the availability of the entity", it can be observed that for event 2 to occur, event 1 must always occur first, i.e., 1 is before 2 and therefore 2 is after 1), by means of timed extensions the TL adds real time restrictions that relate the exact occurrence of those events - Domínguez, A. F. (2018). Master's Thesis.

As in modal logic, the semantics of TL is defined in Kripke structures (a variation of transition systems to represent behaviors of a system) (Laroussinie & Schnoebelen 1995). These structures are used in model checking.

The TL comprises two main frames: linear time and branched time. In a Kripke structure, the linear time frame aims to express the properties along each individual or group trajectory as the case may be, while the branched time frame adds quantification over the possible trajectories.

Its routine application to represent and reason about temporal information, to specify desirable behaviors of computer systems is very useful, and in turn, its ability to verify that certain behavior is fulfilled, as established by a particular specification, is significant during the process of conception of the functional logic of computational processes.

According to Domínguez, A. F. (2018). Master's Thesis, additional applications include the specification of reactive and concurrent systems, formal verification of hardware/software protocols, manual and automatic program composition support, as well as verification of documents and hypermedia applications.

Conclusions

The linear time logic (LTL) modeling is very helpful when diagramming specific processes, where the realization of flows is required in a natural and understandable way, and with the ability to extrapolate to a computational language.

Bibliography

• Garis, A. G. (2010). Temporal logic in software model checking. Origin and evolution to current times. Foundations in Humanities, 11(21), 151-161.
• Kristin Y. Rozier, Linear Temporal Logic Symbolic Model Checking, Computer Science Review, Volume 5, Issue 2, 2011, Pages 163-203, ISSN 1574-0137.
• DOMÍNGUEZ, Alejandro Fernández. Master's Thesis. 2018.