Formal System Specification

• The lecture covers formal specification and modeling in the design and development of secure systems.
• It recalls formal methods, explains formal specification and modeling, and introduces Automata/Finite State Machines.

Learning Objectives

• Recall formal methods and their use in developing secure systems.
• Explain formal specification, how it is applied to system development, and different approaches.
• Describe automata and their use in modeling system behavior.

Formal Methods (FMs)

• FMs are mathematical-based techniques and tools to express a complex system as a mathematical entity.
• FMs can specify, model, and verify the structure/behavior of a system.
• They can be used in any phase of the System Development Life Cycle (SDLC) to detect errors early.

Formal Methods in Development Life Cycle

• Formal Specification: mathematically expresses system requirements and functioning, associated with Informal Specification.
• Formal Modeling: applied to design, development, and maintenance stages to represent structure and behavior.
• Formal Verification: analyses the correctness of the model against the system specification and is complementary to testing.

Formal Specification

• It is a system specification in a mathematical language with well-defined syntax and semantics.
• Helps detect defects or errors and presents the system specification clearly.
• System Specification and System Design steps overlap.
• System requirements and formal specifications are interrelated.
• Clients define early stages while developers/specialists define complete, consistent, precise formal specifications.

Types of Formal Specification

• Algebraic techniques: describe system operations and their relationships.
• Model-based techniques: describe system operations relative to potential state changes.
• Languages capture sequential or concurrent behaviors.

Sequential and Concurrent Formal Languages

• Algebraic with Sequential examples: Larch and OBJ
• Model-based Sequential examples: Z, VDM, and B
• Algebraic Concurrent examples: Lotos
• Model-based Concurrent examples: CSP and Petri Nets

Example of Algebraic Specification

• Includes specification name, imports of lists, and informal descriptions.
• It shows operation signatures and axioms defining operations.
• Example includes functions like Create, Cons, Head, Length, and Tail

Example of Model-Based Specification

• Provides schema name, signature, and predicate with a mathematical representation.
• Example includes "SUGAR_OK", representing the state change conditions

Benefits and Limitations of Formal Specification

• Benefits: provides insights into system requirements/design, guide test case creation, supports automated processing, and offers animation/simulation.
• Limitations: designers/developers lack training, widespread ignorance, research focuses on notations rather than tool support.

Formal Modelling

• Formal modelling specifies the behaviour and structure of a system using a mathematical model
• It uses sequential or concurrent behaviour and structure of core system components

Formal Modelling Languages

• Textual languages
• Graphical languages
• Examples include: Vienna Development Method, Process Algebra, Automata, Petri Nets and Unified Modeling Language (UML)

Finite State Machines (FSMs)

• It can formally specify, verify, and test systems.
• It provides an abstract description of system states and the system's response to external actions.

Communicating Finite State Machines (CFSMs)

• It can receive/send messages and change internal states.
• It can be combined to represent complex behaviors for analysis.

Formal Definition of Communicating Finite State Machines

• CFSMs are expressed as a tuple: F = (Q, q0, A, T).
• Q: finite non-empty set of states.
• q0: initial state (∈ Q).
• A: finite set of communication actions, called the alphabet of F.
  • T: (Q, (A∪{τ})) → Q is the transition relation.

Example of CFSMs

• It is a simple sender-receiver schemes.
• Sender receives a signal on channel a, transmits to Receiver via channel b, using channel b.
• Receiver accepts/forwards the signal using channel c.

CFSMs Initial States

• q0 and r0 represent initial states.
• a? and a! represent receiving/sending over channel a.
• a? & a! are matching messages or signals.

Observations on Example CFSMs

• The concurrent composition of two CFSMs is denoted as System = Sender || Receiver.
• Sender: <> (a?) (a?, b!) (a?, b!, a?) ...
• Receiver: <> (b?) (b?, c!) (b?, c!, b?) ...
• Traces generated by System: 〈〉 〈a?〉 〈a?, b!&b?) (a?, b!&b?, c!) ...
• There are four global states: (q0, r0), (q0, r1), (q1, r0), (q1, r1)
• When executing a? at initial state (q0, r0), the system moves to state (q1, r0).
• When executing τ (b!&b?) at state (q1, r0), it moves to state (q0, r1).
• The concurrent composition of two CFSMs can be represented by the following graph format. (q0, r0) a? c! (q1, r0) (q0, r1) System c! a? (q1, r1)
• a?/c!: external actions.
• Internal or hidden action.
• Treat system verification as: single CFSM or pair of CFSMs, depending on verification requirements.

Summary

• Formal methods explicitly define sequential or concurrent behavior.
• Formal Specification helps early detection of system flaws.
• Formal modeling provides a range of modelling languages.
• FSMs efficiently model system behavior by expressing the state changes that occur during its operation.