References:
https://plato.stanford.edu/entries/logic-temporal/
In order to ensure correct behavior of a reactive program, in which computations are non-terminating (e.g. an operating system), it is necessary to formally specify and verify the acceptable infinite executions of that program. In addition, to ensure correctness of a concurrent program, where two or more processors are working in parallel, it is necessary to formally specify and verify their interaction and synchronization.
Key properties of infinite computations that can be captured by temporal patterns are liveness, safety, and fairness (see Manna and Pnueli 1992):
Liveness properties or eventualities involve temporal patterns of the forms Fp,q→Fp, or G(q→Fp), which ensure that if a specific precondition (q) is initially satisfied, then a desirable state (satisfying p) will eventually be reached in the course of the computation. Examples:
Safety or invariance properties involve temporal patterns of the forms Gp,q→Gp, or G(q→Gp), which ensure that if a specific precondition (q) is initially satisfied, then undesirable states (violating the safety condition p) will never occur. Examples:
Fairness properties involve combinations of temporal patterns of the forms GFp (“infinitely often p”) or FGp (“eventually always p”). Intuitively, fairness requires that whenever several processes that share resources are run concurrently, they must be treated ‘fairly’ by the operating system, scheduler, etc. A typical fairness requirement says that if a process is persistent enough in sending a request (e.g. keeps sending it over and over again), its request will eventually be granted.
An infinite computation is formally represented by a model of the linear time temporal logic LTL. Non-deterministic systems are modeled by branching time structures. Thus, both LTL and the computation tree logics CTL and CTL* have been very important for specification and verification of reactive and concurrent systems.
Linear
References: Monad Brian Beckman: Don’t fear the Monad What is a Monad? - Computerphile Haskell: Monads. A 5-minute introduction Monads Monad: a software design pattern. In functional programming, a monad is a software design pattern with a structure that combines program fragments (functions) and wraps their return values in a type with additional computation. General purpose languages use monads to reduce [boilerplate code] needed for common operations (such as dealing undefined values of fallible functions, or encapsulating bookkeeping code.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?