Accounting for the increasing uncertainties related to forecast of renewables is becoming an essential requirement while assessing the security of future power system scenarios. The FP7 EU project iTesla tackles these needs and reaches several major objectives, including the development of a security platform architecture. In particular, the platform implements a complex stochastic dependence model to simulate a reasonable cloud of plausible “future” states - due to renewable forecast - around the expected state, and evaluates the security on relevant states sampling the cloud of uncertainty. The paper focuses on the proposed model of the uncertainty and its exploitation in power system security assessment process.

This paper addresses the dependability analysis of protection schemes of transmission grids using a computer simulator. Following modern protection schemes, a stochastic hybrid model has been developed in Modelica/Dymola environment. The model supports the evaluation of required dependability on the basis of suitable probability indices. A different simulation strategy has been implemented and its main features are discussed in detail. A logging tool has been created to supervise discrete events and assist in the results analyses. Furthermore, a custom simulation control panel helps to manage and to launch the simulation outside the Modelica environment.

The research described concerns the partitioning of large control applications for a multi-computer system in order to meet plant localization requirements and to exploit parallelism. The considered applications have hierarchical structure and are composed by a network of automata. Our application domain is the automation of power stations and electricity distribution. Because of strong EM noise in such environments, the software architecture is organized to be tolerant to transient faults, which could affect the stability of the control system. The hierarchical structure provides a decompositional approach to the design of complex applications. The context for this work is the ASFA platform, originally designed by the Italian board of electricity. The main result is a new partitioning algorithm for hierarchical automata networks, that splits the application into sub-networks which are deadlock-free, compliant with localization constraints, and as parallelizable as possible. The algorithm is also able to satisfy mutual exclusion constraints and to take into account computation/communication weights to achieve balancing of partitions.

We address the problem of increasing the impact of formal methods in the practice of industrial computer applications. We summarize the reasons why formal methods so far did not gain widespead use within the industrial environment despite several promising experiences. We suggest an evolutionary rather than revolutionary attitude in the introduction of formal methods in the practice of industrial applications, and we report on our long-standing experience which involves an academic institution. Politecnico di Milano, two main industrial partners, ENEL and CISE, and occasionally a few other industries. Our approach aims at augmenting an existing and fairly deeply rooted informal industrial methodology with our original formalism, the logic specification language TRIO. On the basis of the experiences we gained we argue that our incremental attitude toward the introduction of formal methods within the industry could be effective largely independently from the chosen formalism.

This paper presents the TRIO logical framework to specify industrial real-time systems. Typical specification requirements for this kind of system are discussed and related to corresponding features of the framework. In particular, the methodological expressiveness, the validation and the temporal constraint proof capabilities are highlighted. The former is mainly dealt with by the Object Oriented paradigm, while the latter is dealt with by a formal method specification derived from Metric Temporal Logic languages. Further, this Metric Temporal Logic is extended with the ability to treat different granularities. In order to show the capabilities of the TRIO logical framework, the specification of a complex real-time system is proposed.