Input File Formats

From DESUMA Wiki
Input File Formats
Jump to: navigation, search

The description of each element is found in italics with { } directly beside it.


Contents

Individual FSM

The default for each event (transition) is controllable and observable (c and o). If an event is uncontrollable and unobservable, you may specify so after the new state with 'uc' and 'uo'. If the event is either uncontrollable but observable or unobservable but controllable, you may simply state the variable ('uc' or 'uo') that describes the negative characteristic. Please note that you may ignore 'uc' and 'uo' completely if you choose to create the unobservable events file manually by writing this text file. If you choose to use the routine write_uo, you have to state the event properties in the machine.fsm files. Also, the program called "add_prop" adds the uc and uo properties to all events in the FSM file based on the events.uo and events.uc inputs.

4
{# of states}

VC 1/0 4
{State} {Marked/Unmarked} {# of Transitions}

SC1 VSC
{Event} {New State}

CV VC

..... ......

Optionally, additional events not appearing in transitions can be added to a machine. To do this, after the last state and transition, add a new line beginning with the key word EVENTS. After this line, additional events can be listed in the format for an event list. i.e. to add uncontrollable and unobservable event 'a' to an FSM, add the following at he end of the file.

EVENTS

a uc uo


Stochastic Information for an FSM

The machine.stoc file can be created using the create_sfsm routine. You need to have the machine you want to add probabilities to already created.

{FROM STATE name} {TO STATE name} {EVENT name} {Probability}

S1 S2 a 0.5

S1 S2 b 0.5

S2 S4 e 0.7

..... ...... ...... ......

In the above g.ft, we have partitioned {Stuck Closed 1, Stuck Closed 2} as failure type 1 and {Stuck Open 1, Stuck Open 2} as failure type 2.


Sensor Data Map (compose)

The sensor data map contains the state of each sensor for every state of the system. For large systems part of the map creation process can be automated using sensmap. The sensor data map contains one line for each state and corresponding sensor values.


C9, V1, P4, F2, B2, L1 PNP, NF
{State} {Sensor values at this state}

C9, V3, P3, F2, B2, L1 PPP, F

.... .... .... ....


Global Sensor Map for the System (sensmap)

Sensmap is a utility to help automate the creation of sensor data maps for use with the compose routine. For each state in the global sensor map, sensmap searches for states in the system with that state as a substring. It then assigns the corresponding sensor values to that FSM state. The states in the global sensor map must have components ordered the same way as in sync.fsm. 10 {# of pairs of mapping}

P1 PNP, NF
{State Components} {Sensor1, Sensor2} {Assigns all states containing string p1 to have sensor values PNP,NF}

P4 PNP, NF
{State Components} {Sensor1, Sensor2} {Assigns all states containing string P4 to have sensor values PNP, NF}

.... .... .... ....


Events Map for the System (I-Diagnosability)

Events.ift contains information about the indicator events and the failure partition each indicator event detects. 6
{# of pairs mapping}

CV 1
{indicator event} {Failure Type}

OV 2

... ... ... ...


Failure Partition for Building Diagnoser

The g.ft data file can be created from the sync.uo. From the sync.uo, we append the failure type for each unobservable event. SC1 1
{Unobservable Event} {Failure Type}

SC2 1

SO1 2

... ... ... ...

In the above g.ft, we have partitioned {Stuck Closed 1, Stuck Closed 2} as failure type 1 and {Stuck Open 1, Stuck Open 2} as failure type 2.

List of Secret States for Opacity

This file must be created if one wishes to verify opacity of an FSM. Simply list each state in the original FSM that is a secret state. Separate each state with a new line.

state1
state2
...

In the above g.states, we have listed state1 and state2 as being "secret." Thus, when opacity verification is run, the algorithms will take these secret states into account.

List of Initial States for Initial State Opacity

This file must be created if one wishes to verify initial state opacity of an FSM. Since the current state of DESUMA only allows for specification of one initial state, we are extending this to allow for multiple initial states to be specified through an input file. List each state in the original FSM that is an initial state. On the same line as each state listed, followed by a space, specify a 0 or a 1 to designate whether that initial state is a part of the secret set or not (1 meaning yes, 0 meaning no). Separate each state and integer pair with a new line.

state1 0
state2 1
...

In the above g.init, we have listed state1 and state2 as being initial. Furthermore, state1 is not secret because of the 0 accompanying it, and state2 is secret because of the 1 accompanying it. Thus, when initial state opacity verification is run, the algorithms will take into account the multiple initial states that have been specified.

NOTE: By convention, the first state listed in the .fsm file format is the initial state of the fsm. You need not list this state in the list of initial states for the input file, but if you do, it will not be double counted. Note that if you do not list the first state specified in your fsm file, it will still appear in the initial state list but will be defaulted to being non-secret. If you would like it to be secret, make sure to list it in the .init file along with a "1" designation. Be sure that the first state listed in the .fsm file is indeed an initial state.

Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox
EECS @ UM
Tools