| 1. |
- Alenljung, Tord, 1977, et al.
(författare)
-
Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs
- 2012
-
Ingår i: IEEE Transactions on Control Systems Technology. - : Institute of Electrical and Electronics Engineers (IEEE). - 1063-6536 .- 1558-0865. ; 20:6, s. 1506-1521
-
Tidskriftsartikel (refereegranskat)abstract
- This paper introduces Sensor Graphs, a discrete event modeling language directed at physical systems with binary and identity sensors (e. g., RFID). The aim of Sensor Graphs is to simplify the modeling of the plant/process that is to be controlled by a discrete controller, for example a programmable logic controller (PLC); thereby making formal verification and other model-based formal methods more applicable for PLC programmers. The formal syntax and semantics of Sensor Graphs are defined and a compact graphical representation is presented. The language is exemplified by modeling a conveyor module and a lab process. For comparison, the latter is also modeled using Statecharts and Net Condition/Event systems. A controller, modeled as a discrete state equation, can be composed with a Sensor Graph of the process in order to form a model of the closed-loop system. It is demonstrated how requirements on such a closed-loop system, based on a PLC program and a Sensor Graph process model, can be formally verified using the model checker Cadence SMV.
|
|
| 2. |
- Lennartson, Bengt, 1956, et al.
(författare)
-
Efficient Temporal Logic Verification by Incremental Abstraction
- 2020
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. ; 2020-August, s. 894-899
-
Konferensbidrag (refereegranskat)abstract
- A recently formulated incremental abstraction method that preserves CTL∗-X is further developed and evaluated in this paper. The temporal logic CTL∗-X includes both linear temporal logic (LTL) and computational tree logic (CTL), except for the next operator (often denoted by X). For a modular transition system, the incremental abstraction means that any local events, only included in one of the subsystems, are first abstracted. After synchronization more events become local. Repeated abstraction then means that further reduction of local transitions is achieved when more submodels are synchronized. This incremental abstraction is evaluated as a tool for temporal logic verification, and compared with a couple of competitive alternatives. In a preliminary evaluation, the proposed incremental abstraction is often shown to be the most efficient choice for verification of temporal logic properties, especially when some individual submodels are comparatively large.
|
|
| 3. |
- Lennartson, Bengt, 1956, et al.
(författare)
-
State-labeled safety analysis of modular observers for opacity verification
- 2022
-
Ingår i: IEEE Control Systems Letters. - 2475-1456. ; 6, s. 2936-2941
-
Tidskriftsartikel (refereegranskat)abstract
- Verification of opacity and anonymity for modular systems is in this paper formulated as safety analysis of local observers with state labels. A unified modeling strategy is presented based on a generalized synchronous composition, including both shared and non-shared state labels. The proposed modeling approach is shown to be flexible and general, making it possible to solve both local, global, and arbitrarily joint secret state problems simultaneously. A scalable modular n-floor, m-elevator security benchmark problem is also formulated and evaluated by two powerful safety analysis methods. It is shown that current-state opacity for non-trivial complex systems involving more than 1025 observer states can be verified in about one second.
|
|
| 4. |
- Lennartson, Bengt, 1956, et al.
(författare)
-
State-Vector Transition Model Applied to Supervisory Control
- 2012
-
Ingår i: 17th IEEE International Conference on Emerging Technologies & Factory Automation (ETFA). - 9781467347372
-
Konferensbidrag (refereegranskat)abstract
- In supervisory control theory, a supervisor restricts the plant in order to fulfill given specifications. A problem for larger industrial applications is that the resulting supervisor is not easily implemented and comprehensible for the users. To tackle this problem, an efficient method has recently been introduced to characterize a supervisor by tractable logic conditions, referred to as guards. This approach has been developed for a specific type of automata with variables called extended finite automata (EFAs). An extension of this approach to a more general class of models is presented in this paper. It means that classical supervisory control problems for automata and Petri nets are easily and efficiently solved, but also generalized based on the suggested approach. The synthesis procedure is naturally modeled and efficiently computed based on binary decision diagrams.
|
|
| 5. |
- Lennartson, Bengt, 1956, et al.
(författare)
-
Supervisory Control for State-Vector Transition Models—A Unified Approach
- 2014
-
Ingår i: IEEE Transactions on Automation Science and Engineering. - 1558-3783 .- 1545-5955. ; 11:1, s. 33-47
-
Tidskriftsartikel (refereegranskat)abstract
- A generic state-vector transition (SVT) model is suggested, including a flexible synchronous composition involving both shared variables and events. This model is analyzed, focusing on properties that are important for supervisor synthesis. A synthesis procedure is then developed for the SVT model, where supervisor guards are generated that guarantee a controllable, nonblocking and maximally permissive supervisor. Novel conditions are introduced, such that more flexible specifications can be applied than earlier suggested for related models. Since the SVT model includes automata and (colored) Petri nets, optionally extended with variables, guards and actions, as special cases, the suggested synthesis approach unifies supervisor synthesis for the main discrete event model classes. Finally, the SVT model is naturally represented and efficiently computed based on binary decision diagrams, and the resulting supervisor guards are easily implemented in industrial control systems.
|
|
| 6. |
- Lennartson, Bengt, 1956, et al.
(författare)
-
Visible Bisimulation Equivalence - A Unified Abstraction for Temporal Logic Verification
- 2018
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 51:7, s. 400-407
-
Konferensbidrag (refereegranskat)abstract
- Bisimulation is an abstraction method that can be used to reduce the number of states for transition systems. This paper presents an alternative formulation of bisimulation, directly based on an equivalence relation and partitioning of the state space. The formulation, here called visible bisimulation equivalence, unifies stuttering and branching bisimulation by including both state and event labels in the abstraction. The proposed divergence-sensitive visible (DSV) bisimulation equivalence is shown to be equivalent to a temporal logic called ECTL, where CTL is extended with events. This means that DSV bisimulation equivalence preserves most temporal temporal logic properties that are of interest. The proposed bisimulation abstraction is applied to a set of synchronized submodels, where local events are identified incrementally and abstracted after each synchronization. Since the bisimulation reduction is applied after each synchronization, a significant part of the state space explosion in ordinary synchronization is avoided. Since the abstraction is polynomial in the number of states and transitions, this is an attractive method for verification and synthesis based on temporal logic.
|
|
| 7. |
- Makki, Behrooz, 1980, et al.
(författare)
-
An evolving neural network to perform dynamic principal component analysis
- 2009
-
Ingår i: Neural Computing and Applications. - : Springer Science and Business Media LLC. - 0941-0643 .- 1433-3058. ; 19:3, s. 459-463
-
Tidskriftsartikel (refereegranskat)abstract
- Nonlinear principal component analysis is one of the best dimension reduction techniques developed during the recent years which have been applied in different signal-processing applications. In this paper, an evolving category of auto-associative neural network is presented which is applied to perform dynamic nonlinear principal component analysis. Training strategy of the network implements both constructive and destructive algorithms to extract dynamic principal components of speech database. In addition, the proposed network makes it possible to eliminate some dimensions of sequences that do not play important role in the quality of speech processing. Finally, the network is successfully applied to solve missing data problem.
|
|
| 8. |
|
|
| 9. |
- Makki, Behrooz, 1980, et al.
(författare)
-
Modeling Superconductive Fault Current Limiter using Constructive Neural Networks
- 2007
-
Ingår i: IEEE symposium on Industrial Electronics-ISIE. - 9781424407552 ; 1:1, s. 2859-2863
-
Konferensbidrag (refereegranskat)abstract
- Although so many advances have been proposed in the field of artificial intelligence and superconductivity, there are few reports on their combination. On the other hand, because of the nonlinear and multivariable characteristics of the superconductive elements and capabilities of neural networks in this field, it seems useful to apply the neural networks to model and control the superconductive phenomena or devices. In this paper, a new constructive neural network (CNN) trained by two different optimization algorithms; back-propagation and genetic algorithm, is proposed which models the behavior of the superconductive fault current limiters (SFCLs). Simulation results show that the proposed approach is in good harmony with the real characteristics of the SFCLs.
|
|
| 10. |
- Makki, Behrooz, 1980, et al.
(författare)
-
Principal Component Analysis using Constructive Neural Networks
- 2007
-
Ingår i: International Joint Conference on Neural Networks. - 1098-7576. - 9781424413805 ; 1:1, s. 558-562
-
Konferensbidrag (refereegranskat)abstract
- In this paper, a new constructive auto-associative neural network performing nonlinear principal component analysis is presented. The developed constructive neural network maps the data nonlinearly into its principal components and preserves the order of principal components at the same time. The weights of the neural network are trained by a combination of back propagation (BP) and genetic algorithm (GA) which accelerates the training process by preventing local minima. The performance of the proposed method was evaluated by means of two different experiments that illustrated its efficiency.
|
|
