Formal and logical models for functional requirements

By Timur Galimov, tishgalimov@edu.hse.ru

In today's world, technology is playing an increasingly important role, software development is becoming an increasingly complex task. One of the key aspects of software development is the functional requirements that define what the system should do and how it should interact with the user. To define these requirements, formal and logical models are used to help developers create more efficient and understandable systems.

First of all, let's deal with the basic concepts that will be discussed later:

Functional requirements are a description of what the system should do, what functions and capabilities should be implemented. They determine the functionality of the system and its behavior in response to various input data and user actions.

Formal models of functional requirements are mathematical methods and tools used to describe functional requirements for a system. These are format specifications that describe the behavior of the system in terms of mathematical expressions and logical operations. For example, one of the most common formal models is the finite state machine model, which describes the behavior of a system in terms of states and transitions between them. Another common model is the Petri net model, which is used to describe parallel processes and interactions between them.

Logical models of functional requirements are used to define logical rules and conditions governing the behavior of the system. They help developers determine how the system will respond to different inputs and what actions can be performed in different situations. One of the most common types of logical models is the truth table, which provides a systematic way to determine the various possible outcomes for a given set of input data. It is important to choose the appropriate models for the system being developed and ensure their consistent use throughout the development process.

As mentioned earlier, formal methods are a group of methods based on mathematical models that are used to describe functional requirements. Their use is dictated by the desire to improve the reliability of systems, but they are quite complex, require special training and investment of time and resources only because of the use of mathematical models.

Formal models of functional requirements can be presented in different ways, depending on the specific task and system requirements. Let's look at some common methods below – Petri nets, a use case diagram, and a state transition diagram. Let's look at each in more detail.

Petri nets are graphical models used to describe systems characterized by parallelism, synchronization, and competition for resources. These models facilitate visualization of system states, transitions and dependencies, helping in requirements analysis and verification. They consist of two main components: positions and transitions. Positions are locations where markers (tokens) can be located, indicating the presence of certain resources or conditions in the system. Transitions are events that can occur in the system and change the state of the system by moving tokens from one position to another. Modeling a system using a Petri net involves determining the positions, transitions and connections between them, as well as setting initial and final conditions. Once a network is created, you can analyze its behavior, for example, determine a possible sequence of events, find constraints and conflicts, and evaluate system performance. One of the advantages of Petri nets is their simplicity and visibility, which makes it easy to understand and visualize the simulated systems. In addition, they are highly flexible and can be adapted to simulate various types of systems, including parallel and distributed systems, systems with constraints and systems with asynchronous events.

One of the most common formal models used in the development of functional requirements is the use case diagram. This model provides a visual representation of the various actors and activities that are involved in the operation of the system, helping to identify the key characteristics and functions that need to be enabled. The use case diagram consists of actors, use cases, and the relationships between them.

For example, consider an online shopping system. The actors in this system can be buyers, sellers and administrators. Use cases may include searching for products, adding products to the cart, placing an order, and managing orders. The relationships between participants and usage scenarios show how they interact with each other, for example, how customers add items to the cart or how administrators manage orders.

Another important formal model is the state transition diagram. This model allows you to determine the various states in which the system can be located, and the conditions under which it will move from one state to another. This is especially important for systems with multiple states, such as complex production processes or financial systems. A state transition diagram consists of states, events, and transitions between them. States represent certain states or modes of operation in which the system can be located. Events cause a state change, and transitions represent a transition from one state to another.

For example, consider a vending machine. The states of this system can be as follows: idle, waiting for payment, delivery of goods, failure. Events may include coin insertion, product selection, and product issuance. Transitions show how the system moves from one state to another, for example, how it moves from waiting for payment to issuing a product.

Logical models are also necessary when developing functional requirements. These models help to define the logical rules and conditions that determine the behavior of the system. For example, a logical model can define rules for accessing certain types of data or conditions under which certain actions can be performed.

One of the most common types of logical models is the truth table. This model is a systematic way to determine the various possible outcomes for a given set of input data. This can be especially useful in systems with complex decision-making processes, for example, in medical diagnostics or financial analysis.

The truth table consists of inputs, outputs, and logical operators. Inputs are variables or conditions that affect the outcome of the system. The outputs represent the result of the system operation based on the input data. Logical operators define how inputs are combined to produce a result.

For example, consider a system that determines whether a patient has a certain disease based on his symptoms. At the entrance, there may be symptoms such as fever, cough and fatigue. At the exit, a diagnosis can be made - the presence or absence of the disease in the patient. Logical operators define how input data is combined to produce an output result, for example, it is required that a certain number of symptoms are present before diagnosis.

Formal and logical models are important tools for developing functional requirements for any system. They help define the rules and conditions that govern the behavior of the system, ensuring that it meets the needs of its users and stakeholders. Formal models allow you to visualize and analyze requirements, while logical models, presented in the form of logical expressions and predicates, provide control over the correctness and completeness of these requirements. The integration of formal and logical models with behavioral and data models allows developers to create a more complete and holistic view of the system, which, in turn, improves the quality of the product being developed.

1. Victor Kuliamin, Requirements formalisation on practice, https://www.researchgate.net/publication/256494079_Formalizacia_trebovanij_na_praktike
2. Manfred Broy, A logical approach to systems engineering artifacts: semantic relationships and dependencies beyond traceability—from requirements to functional and architectural views, https://www.researchgate.net/publication/319857343_A_logical_approach_to_systems_engineering_artifacts_semantic_relationships_and_dependencies_beyond_traceability-from_requirements_to_functional_and_architectural_views
3. А. Якобсон, Г. Буч, Дж. Рамбо. Унифицированный процесс разработки программного обеспечения. СПб.: Питер, 2002.
4. Guide for Developing System Requirements Specifications. New York: IEEE, 1998
5. Вигерс К., Битти Дж. Разработка требований к программному обеспечению
6. https://ru.wikipedia.org/wiki/Формальные_методы
7. Kozachok A. V., Bochkov M.V., Lai M.T., Kochetkov E. V., first order logic for program code functional requirements description, DOl: 10.21581/2311-3456-2017-3-2-7