Title: Formal approach for the development of intelligent industrial control components

Authors: Mohamed Khalgui; Olfa Mosbahi

Addresses: Martin-Luther-Universität Halle Wittenberg, Institut für Informatik, Raum 324, Von-Seckendorff-Platz 1 06120 Halle (Saale), Germany. ' Martin-Luther-Universität Halle Wittenberg, Institut für Informatik, Raum 324, Von-Seckendorff-Platz 1 06120 Halle (Saale), Germany

Abstract: The paper deals with reconfigurable embedded control systems following component-based technologies and/or Architecture Description Languages (ADL). A Control Component is defined as a software unit of the system which is assumed to be a network of components with precedence constraints. We define an agent-based architecture to handle automatic reconfigurations under well-defined conditions by creating, deleting or updating components to dynamically bring the whole system into safe and optimal behaviors. To cover all reconfiguration forms, we model the agent by nested state machines according to the formalism Net Condition/Event Systems (NCES), and apply a model checking to verify properties of NCES according to the temporal logic "Computation Tree Logic" (CTL). The goal is to check the agent's reactivity after any environment's evolution. Several complex networks can implement the system such that each one is executed at a given time when a corresponding reconfiguration scenario is automatically applied by the agent. To check the correctness of each one of them, we apply in several steps a refinement-based approach that automatically specifies feasible Control Components according to NCES. The model checker SESA is automatically applied in each step to verify deadlock properties of new generated components, and is manually used to verify CTL-based properties according to user requirements. We implement the proposed agent by three modules that allow interpretations of environment's evolutions, decisions of useful reconfiguration scenarios before their real applications.

Keywords: embedded control systems; reconfiguration; agent-based architecture; model-checking; Petri nets; CTL; computation tree logic; implementation; intelligent control; control components; agent-based systems; multi-agent systems; net condition-event systems.

DOI: 10.1504/IJCAT.2011.045400

International Journal of Computer Applications in Technology, 2011 Vol.42 No.2/3, pp.84 - 107

Published online: 11 Feb 2012 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article