This case study analyses the possibilities to improve the execution time of model-based developed software by applying optimisations during code generation and compilation. The present case study is performed on flight control software, for which safety aspects are accounted throughout the development. Therefore, a formally verified compiler is used for the optimisation during the compilation. The optimisation is evaluated by execution time measurements on the target and a static worst-case execution time analysis. Based on the results, recommendations for certain model patterns are given, which impact the worst-case execution time analysis.

We present LhaVrf, a symbolic verifier for the safety verification of concurrent LHA (Linear Hybrid Automaton). A concurrent LHA is composed of a set of LHAs that interact through shared variables and/or events. An LHA is first translated to a purely discrete linear transition system that preserves the reachability of discrete states. Its analysis can be conducted in the proposed counterexample fragment based specification relaxation (CEFSR) framework, where an invalid fragment of a counterexample is used to eliminate the entire set of counterexamples sharing the same fragment, by way of specification relaxation (as opposed to the traditional model refinement). For concurrent systems, we propose further enhancement towards scalability as follows. For each spurious counterexample, an unsatisfiable core (unsat-core) that makes the counterexample invalid, is identified and used for specification relaxation, thereby eliminating the entire set of spurious counterexamples sharing the same unsat-core in a single iteration. Our implementation of LhaVrf adopts the above key ideas, with capability of automatically translating the hybrid automata into discrete transition system, composing the concurrent model, and using satisfiability modulo theory solver for validating counterexamples and fast-searching for the unsat-core. The verifier is illustrated via an application to the Fischer mutual exclusion protocol.

This study presents a demand side management (DSM) strategy for a cyber-physical smart distribution system (CPSDS). The proposed approach uses the price-based as well as reward-based DSM schemes as a part dual objective function. The objectives of the proposed scheduling approach comprise the profit maximisation objectives of demand response aggregator agent (DRAA) and network performance objectives of the distribution system operation agent. The same are achieved by providing incentives to the participating customers. The incentive information is communicated to responsive load agent (RLA) using cyber infrastructure (communication channels, sensors and cloud storage systems) and thus allowing customers to select the incentive program of their own choice as per their flexibility. The real-time implementation of the program is considered to have direct load control based once the event trigger acknowledgement is received by DRAA/utility from RLA for control action on responsive loads. The proposed price-based and reward-based DSM framework in CPSDS is evaluated using IEEE 37 bus test system. The simulation results of proposed dual objective price-based and reward-based mechanism are presented, discussed and compared with single objective price-based approach. The same demonstrates the improved tradeoff between techno-economic aspects of distribution system operation.

Despite the growing deployment of mission critical applications on computing systems, trust and security continues to hinder its full adoption and deployment on cloud computing platforms. In addition to accountability and non-repudiation on the cloud deployment, end-users want to be confident of availability and reliability of services. For any cloud platform to be secure and trusted, the individual layers of the platform must be secure as there is no ‘one fits all solution’ for securing all the layers. This work presents a multi-layer trust security model (MLTSM) based on unified cloud platform trust that employs a fuzzy logic combination of on-demand states of several different security mechanisms, such as identification, direct and in-direct trust, across all cloud layers. In addition, results from a MATLAB-based simulation of the model are also presented. A MLTSM can improve the secure deployment of cloud infrastructure in mission critical sectors such as electrical power system operation, as it provides empirical evidence that allows direct (on-demand) determination and verification of the trust state of any given cloud computing platform or service. Such a modelling approach is useful for comparison, classification and improving end-user confidence in selecting or consuming cloud computing resources.

Cyber physical systems like smart grid are largely migrating towards distributed control philosophy to achieve high reliability. The design of communication network between various sensors and controllers plays an important role in control of these systems. The design process involves examining a number of topological combinations, which increase exponentially with the number of nodes in the considered system. Moreover, for a practical system, the different characteristics and availability of various physical and communication resources in the network pose multiple constraints on this design. In this work, a generalised constraint-based sensor controller connection design methodology has been developed, which effectively reduces the number of combinations, to design more stable cyber-physical controllers. To handle variations in multiple parameters in physical and communication domain, different controllers have been developed for different operating conditions that are scheduled as per requirement. The methodology has been shown to stabilise bus voltages in a smart grid scenario under variations in load, communication delays and loss of communication links.