Z lecture notes: Modeling Large Systems

This page looks best when this and this X are about the same size: X. See these viewing tips.

Large systems are composed of components collected into subsystems. Complex components can be built up from simpler ones using schema inclusion.

$\begin{schema}{$		Param



		preset, setpoint, value: SIGNAL

	$\end{schema}$

$\begin{schema}{$		PS



		Param
		contactor: SWITCH
		faults: $\power$ FAULT

	$\where$

		faults $\neq$ $\emptyset$ $\implies$ setpoint = 0
		contactor = open $\implies$ setpoint = 0
		...

	$\end{schema}$

On $\defs$ [ PS | contactor = closed ... ]

TurnOn $\defs$ Off $\land$ (On' $\lor$ Error')

Servo $\defs$ [ Param; enable: MODE; ... | ... ]

Each component has a name. Components have different types but they all have the same type of name. Names of similar components are collected into sets. The state of the entire system is a collection of functions from names to bindings of the component types.

[NAME]

ps = { rf, mainfld, ... }

s = { mainprb, deflprb, ... }

$\begin{schema}{$		Cyclotron



		supply: ps $\fun$ PS
		servo: s $\fun$ Servo
		...

	$\where$

		...

	$\end{schema}$

Operations on single components can be promoted to operations on the whole system. First define a framing schema.

$\begin{schema}{$		CycloFramePS



		$\Delta$ Cyclotron
		$\Delta$ PS
		ps?: ps

	$\where$

		{ ps? } $\ndres$ supply' = { ps? } $\ndres$ supply
		$\theta$ PS = supply ps? $\land$ $\theta$ PS' = supply' ps?

	$\end{schema}$

Then combined the component operation with the frame, identifying the component of interest.

$\begin{schema}{$		TurnOnMainfld



		CycloFramePS
		TurnOn

	$\where$

		ps? = mainfld

	$\end{schema}$

Subsystems can be modelled by sets of names of dissimilar objects. States and operations can be defined on subsystems.

$\begin{axdef}$
		rfsys, cyclo, bla, blb, blc, iso, fix: $\power$ NAME
	$\end{axdef}$

$\begin{schema}{$		TurnOnBLA



		$\Delta$ Cyclotron

	$\where$

		$\forall$ p: ps $\cap$ bla $\exists$ TurnOn
		$\theta$ PS = supply p $\land$ $\theta$ PS' = supply' p

	$\end{schema}$

$\begin{schema}{$		BLAReady



		Cyclotron

	$\where$

		supply $\limg$ ps $\cap$ bla $\rimg$ $\subseteq$ On

	$\end{schema}$

$\begin{schema}{$		SafeTurnOnBeam



		TurnOnBeam

	$\where$

		IsoTest $\implies$ CycloReady $\land$ BLAReady
		$\land$ IsoReady

		IsoTreat $\implies$ CycloReady $\land$ BLAReady
		$\land$ IsoSafe

		Preconditions for other modes ...


	$\end{schema}$

T_TurnOnBeam $\defs$ SafeTurnOnBeam $\lor$ (Interlocked $\land$ $\Xi$ Cyclotron)

Schema inclusion is much like inheritance in object-oriented programming languages, but every schema type is distinct (no ``subtypes'').

Param $\defs$ [ preset, setpoint, value: SIGNAL ]

PS $\defs$ [ Param; contactor: SWITCH; ... ]

$\begin{axdef}$
		panel: Param
		mainfld: PS

	$\where$

		panel.setpoint = mainfld.setpoint
	$\end{axdef}$

`offset == ( Param value - setpoint)`	Definition
`offset panel`	Type correct
`offset mainfld`	Type error!

MODELING LARGE SYSTEMS