========================================= MODEL: pdist.smv, sat_pdist.xml AUTHOR: Marco Bozzano ========================================= A model of a controller for a power distribution system. MODEL ===== The model is inspired by the power distribution system described in: [1] P.Bertoli, A.Cimatti, J.Slaney, S.Thiebaux. "Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking". Proceedings of 15th European Conference on Artificial Intelligence (ECAI'02). IOS Press, Amsterdam, The Netherlands, 2002. A power distribution system is a network of electric lines connected by switching devices and fed by circuit-breakers. Switching devices and circuit-breakers are connected to at most two lines an have two possible positions: closed or open. When a circuit-breaker is closed, it supplies power to the network, and this power propagates downstream until an open switching device stops the propagation. The positions of the devices are initially set so that each circuit-breaker feeds a given area of the network, with no line being fed by more than one circuit-breaker. Permanent faults can affect one or more lines of the network. When a line is faulty, the circuit-breaker feeding this line opens in order to protect the rest of its area from overloads. As a result, not just the faulty line but the entire area is left without power. The supply restoration problem consists in reconfiguring the network by opening and closing devices so as to electrically isolate the faulty lines and re-supply a maximum of non-faulty lines on the lost areas. We model the "Simple" topology described in [1]. The network is composed of three circuit breakers (CB1, CB2, CB3), seven switching devices (SD1, SD2, SD3, SD4, SD5, SD6, SD7), and seven lines, four lines with two connections (L1, L3, L5, L7) and three lines with three connections (L2, L4, L6). The network is initialized as follows: CB3 [ ] .......................................( ) SD3 L7 x x x x x x L5 L6 x CB2 [X] xxxxxxxx(X)xxxxxxxxxxxxxxxxx(X)xxxxxxxxxx L4 SD4 x SD2 x x x x x ( ) SD7 x : x : x SD6 : SD5 x CB1 [ ] ........(X).................( )xxxxxxxx(X) SD1 L1 L2 L3 [ ] = circuit breaker (open) [X] = circuit breaker (closed) ( ) = switching device (open) (X) = switching device (closed) ... = line (not being fed) xxx = line (being fed) The model includes module both for the physical system and the controller. The physical system is composed of of the following modules: - circuit breakers, that feed the lines - switches, that connect two adjacent lines - lines (can be with two or three connectors) The controller takes as input the status of all components of the system. In order to recover from faliures of lines, it begin a recovery procedure consisting in the reconfiguration of the network. The network must always satisfy some safety and liveness requirements (see below). See further comments in the source file. FAILURE MODES ============= - line_2 stuck faulty type = "stuck_at_faulty" NuSMV node: line_2.status description: a faulty line with two connections - line_3 stuck faulty type = "stuck_at_faulty" NuSMV node: line_3.status description: a faulty line with three connections SAFETY REQUIREMENTS =================== - CTL property formula = "AG (L1.status != broken & L2.status != broken & L3.status != broken & L4.status != broken & L5.status != broken & L6.status != broken & L7.status != broken)" description: no line ever gets broken - LTL property formula = "G F (NR_OPERATIONAL_LINES >= 4)" description: At least 4 lines are always operational (eventually) - LTL property formula = "(G NR_FAILURES <= 1) -> G F (NR_OPERATIONAL_LINES >= 4)" description: In case only single failures can happen, at least 4 lines are always operational (eventually) - PROP formula for FAULT TREE generation formula: "CTRL.status = finished & NR_OPERATIONAL_LINES < 4" description: we want to investigate which failure events can cause less than 4 lines to be operational, after the network reconfiguration performed by the controller