The study aims to address the challenge of dynamic assessment in power systems by proposing a design scheme for an intelligent adaptive power distribution system based on runtime verification.The system architecture i...The study aims to address the challenge of dynamic assessment in power systems by proposing a design scheme for an intelligent adaptive power distribution system based on runtime verification.The system architecture is built upon cloud-edge-end collaboration,enabling comprehensive monitoring and precise management of the power grid through coordinated efforts across different levels.Specif-ically,the study employs the adaptive observer approach,allowing dynamic adjustments to observers to reflect updates in requirements and ensure system reliability.This method covers both structural and parametric adjustments to specifications,including updating time protection conditions,updating events,and adding or removing responses.The results demonstrate that with the implementation of adaptive observers,the system becomes more flexible in responding to changes,significantly enhancing its level of efficiency.By employing dynamically changing verification specifications,the system achieves real-time and flexible verification.This research provides technical support for the safe,efficient,and reliable operation of electrical power distribution systems.展开更多
We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware an...We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software.The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace.We propose a model-based approach that relies on domain specific languages(DSL).A first DSL,called TISL(trace item specification language),captures the relevant data structures.A second DSL,called STML(simulation trace mapping language),abstracts the simulation raw data into logical clocks,abstracting simulation data into relevant observation probes and thus reducing the trace streams size.The third DSL,called TPSL,defines a set of behavioral patterns that include widely used temporal properties.This is meant for users who are not familiar with temporal logics.Each pattern is transformed into an automata.All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated.The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve.We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes,thus reducing the verification time.展开更多
基金supported by the China Electric Power ResearchInstitute and Electric Power Research Institute State Grid AnhuiElectric Power Co.,Ltd.,China(5400-202355201A-1-1-ZN).
文摘The study aims to address the challenge of dynamic assessment in power systems by proposing a design scheme for an intelligent adaptive power distribution system based on runtime verification.The system architecture is built upon cloud-edge-end collaboration,enabling comprehensive monitoring and precise management of the power grid through coordinated efforts across different levels.Specif-ically,the study employs the adaptive observer approach,allowing dynamic adjustments to observers to reflect updates in requirements and ensure system reliability.This method covers both structural and parametric adjustments to specifications,including updating time protection conditions,updating events,and adding or removing responses.The results demonstrate that with the implementation of adaptive observers,the system becomes more flexible in responding to changes,significantly enhancing its level of efficiency.By employing dynamically changing verification specifications,the system achieves real-time and flexible verification.This research provides technical support for the safe,efficient,and reliable operation of electrical power distribution systems.
基金supported by the Sino-European LIAM A Laboratory and by the INRIA Sophia Antipolis Research Center.
文摘We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software.The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace.We propose a model-based approach that relies on domain specific languages(DSL).A first DSL,called TISL(trace item specification language),captures the relevant data structures.A second DSL,called STML(simulation trace mapping language),abstracts the simulation raw data into logical clocks,abstracting simulation data into relevant observation probes and thus reducing the trace streams size.The third DSL,called TPSL,defines a set of behavioral patterns that include widely used temporal properties.This is meant for users who are not familiar with temporal logics.Each pattern is transformed into an automata.All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated.The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve.We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes,thus reducing the verification time.
