IET Cyber-Physical Systems: Theory & Applications
Volume 2, Issue 2, July 2017
Volumes & issues:
Volume 2, Issue 2
July 2017
-
- Author(s): Huafeng Yu ; Stanley Bak ; Xin Li ; Corina Pasareanu ; Ramesh S ; Qi Zhu
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 55 –56
- DOI: 10.1049/iet-cps.2017.0092
- Type: Article
- + Show details - Hide details
-
p.
55
–56
(2)
- Author(s): Kajetan Nürnberger ; Markus Hochstrasser ; Florian Holzapfel
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 57 –64
- DOI: 10.1049/iet-cps.2016.0046
- Type: Article
- + Show details - Hide details
-
p.
57
–64
(8)
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.
- Author(s): Hao Ren ; Jing Huang ; Shengbing Jiang ; Ratnesh Kumar
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 65 –74
- DOI: 10.1049/iet-cps.2016.0042
- Type: Article
- + Show details - Hide details
-
p.
65
–74
(10)
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.
Guest Editorial
Execution time analysis and optimisation techniques in the model-based development of a flight control software
Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata
-
- Author(s): K. Srikanth Reddy ; Lokesh Panwar ; B.K. Panigrahi ; Rajesh Kumar ; Hao Yu
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 75 –83
- DOI: 10.1049/iet-cps.2017.0008
- Type: Article
- + Show details - Hide details
-
p.
75
–83
(9)
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.
- Author(s): Mary-Jane Sule ; Maozhen Li ; Gareth Taylor ; Clement Onime
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 84 –89
- DOI: 10.1049/iet-cps.2017.0016
- Type: Article
- + Show details - Hide details
-
p.
84
–89
(6)
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.
- Author(s): Meher Preetam Korukonda ; Swaroop Ranjan Mishra ; Anupam Shukla ; Laxmidhar Behera
- Source: IET Cyber-Physical Systems: Theory & Applications, Volume 2, Issue 2, p. 90 –100
- DOI: 10.1049/iet-cps.2017.0024
- Type: Article
- + Show details - Hide details
-
p.
90
–100
(11)
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.
Demand side management with consumer clusters in cyber-physical smart distribution system considering price-based and reward-based scheduling programs
Fuzzy logic approach to modelling trust in cloud computing
Handling multi-parametric variations in distributed control of cyber-physical energy systems through optimal communication design
Most viewed content
Most cited content for this Journal
-
Cyber-physical attacks and defences in the smart grid: a survey
- Author(s): Haibo He and Jun Yan
- Type: Article
-
Enabling cyber-physical communication in 5G cellular networks: challenges, spatial spectrum sensing, and cyber-security
- Author(s): Rachad Atat ; Lingjia Liu ; Hao Chen ; Jinsong Wu ; Hongxiang Li ; Yang Yi
- Type: Article
-
Design optimisation of cyber-physical distributed systems using IEEE time-sensitive networks
- Author(s): Paul Pop ; Michael Lander Raagaard ; Silviu S. Craciunas ; Wilfried Steiner
- Type: Article
-
Cybersecurity for distributed energy resources and smart inverters
- Author(s): Junjian Qi ; Adam Hahn ; Xiaonan Lu ; Jianhui Wang ; Chen-Ching Liu
- Type: Article
-
Remote health care cyber-physical system: quality of service (QoS) challenges and opportunities
- Author(s): Tejal Shah ; Ali Yavari ; Karan Mitra ; Saguna Saguna ; Prem Prakash Jayaraman ; Fethi Rabhi ; Rajiv Ranjan
- Type: Article