Here you can find some examples showing that the ability of expressing properties that count occurrences of actions allows for a cleaner separation between the behavioural models and the required properties. For each model, there are the corresponding FSP specification and an informal description and the CFLTL formula of the property to be analysed.
--- Single lane bridge ---
Single Lane Bridge Problem is a modelling problem introduced in [J. Magee and J. Kramer] (cf. Section 7.2 therein). The problem consists of a narrow bridge which only allows for a single lane of traffic, which must be appropriately controlled to avoid safety violations. As one may expect, a safety violation occurs if two cars moving in different directions are on the bridge at the same time. In order to simplify the presentation of the problem, cars moving in different directions are represented by different colours; more precisely, red cars will move in one direction, while blue cars will move in the opposite one. The safety property associated with this model requires expressing that it should never be the case that red and blue cars are on the bridge at the same time. As an extension to the original model, assume that the bridge has a maximum weight capacity. Now another safety property to express is the fact that the controller ensures the bridge's safety, i.e., that the number of cars on the bridge never exceeds the bridge's capacity.
--- Automated teller machine ---
Consider the model of an ATM machine taken from [S. Uchitel et.al.]. Initially, the ATM requests the user to insert a card and enter the password. The validity of the password is verified, and if its verification succeeds, the user can extract money and remove the card from the ATM. Otherwise, when the password is incorrect, the ATM system starts counting the number of successive mistakes made by the user. In case the user makes three consecutive mistakes, the ATM locks the account, preventing money extractions. Notice that the user is able to remove its card form the ATM, provided that his account is not locked. A typical security mechanism that ATMs implement consists of blocking account access when the user makes three consecutive mistakes at entering his password. Two interesting properties are: that it cannot be the case that, after three consecutive wrong password insertions, the user extracts his money, and that the account cannot be locked when less than three incorrect password insertions have happened.
--- TCP Sliding Window ---
Consider the TCP network protocol [Tanenbaum], a reliable delivery service that guarantees that all packages received will be identical with packages sent. The system specification describe the behaviour of a single package along a TCP network communication. Initially, the package that encapsulates the sender's information is waiting to be sent. Once the package is sent, two situations have to be considered: the package can be lost in the communication, or it can be received by the receiver. When the sending fails, a timeout waiting for the acknowledgement will occur, so then the sender resends the package to avoid the loss of packages. In the case of a successful reception, the receiver processes the package and returns an ack (acknowledge) to the sender. If the ack message gets lost, a timeout occurs in the sender and it resends the (not acknowledged) package. In this situation, the receiver will discard the duplicated package. The traffic in a network is specified combining the behaviour of various packages.
The TCP protocol has been improved many times, to optimize network transfer. In particular, the TCP Sliding Window protocol modifies dynamically the size of the window depending on the channel reliability. The term window refers to the number of packages that can be sent without receiving their corresponding acks. In this specification, the protocol considers that initially the window size is 1 and each time that an ack is received, the window size is incremented by one (i.e., the channel's reliability is increased), until the maximum size for the window is reached (in our case, assume 5 packages). When any loss in the channel is detected, i.e., when a timeout occurs, the channel becomes less reliable, so then the window size is decremented by 1 (when it is greater than 1).
At first time, a safety property to check should be that the sender can be waiting at most for MAX acks. An stronger and more appropriated property would be that the number of packages not acknowledged is bounded by the current window size. This stronger property needs to refer to a dynamic value that changes as the system is executing.
--- Golf Club Program ---
The Golg Club Program is a modelling problem introduced in [J. Magee and J. Kramer] (cf. Section 9.1 therein). The problem consists of a golf club which has a limited number of golf balls available for hire. Players can hire golf balls for their game from the club and return them to the club after use. There are two kind of players, experts who tend not to lose any of their golf balls (one or two) and novice players who hire more balls. Due to the unitary nature of the increment or decrement of counting fluents, some minor change was introduced to the original model when the players get[n] and put[n] balls. When one of those events occur, the system perform n times the respective unitary get or put event. An interesting invariant property to check is that the amount of balls available is equal to the difference between the balls stock and those that was given to the players.
