PSL/A Practical Introduction to PSL/Basic Temporal Properties/ru
Основные временные свойства While
В то время как Булевый слой состоит из Булевых выражений, которые выполняются или не выполняются в данном цикле, временной слой предоставляет путь для описания взаимоотношений между Булевыми выражениями по времени. PSL утверждение обычно представлено только в одном направлении - вперед, от первого цикла (также можно двигаться в обратном направлении, используя встроенные функции, такие как prev(), rose() и fell()). Таким образом, простое PSL утверждение assert a; показывает, что a должно утверждаться в самом первом цикле, в то время как PSL утверждение assert always a, показывает, что a должно утверждаться в перовм цикле и в каждом следующем цикле, а это значит, что в каждом цикле.
Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому одтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”,
The temporal layer is composed of the Foundation Language (FL) and the Optional Branching Extension (OBE). The FL is used to express properties of single traces, and can be used in either simulation or formal verification. The OBE is used to express properties referring to sets of traces, for example “there exists a trace such that ...”, and is used in formal verification. In this book we concentrate on the Foundation Language.
The Foundation Language itself is composed of two complementary styles – LTL style, named after the temporal logic LTL on which PSL is based, and SERE style, named after PSL’s Sequential Extended Regular Expressions, or SEREs. In this chapter we present the basic temporal operators of LTL style. We provide only a taste – enough to get the basic idea and to give some context to the philosophical issues that we discuss next.
Throughout this book, we make extensive use of examples. Each example property or assertion and its associated timing diagram (which we term a trace) are grouped together in a figure. Such a figure will contain one or more traces numbered with a parenthesized lower case Roman numeral, and one or more properties numbered by appending a lower case letter to the figure number. For instance, Figure 2.1 contains Trace 2.1(i) and Assertions 2.1a, 2.1b, and 2.1c.
