储能可解决新型电力系统中调峰能力不足、频率不稳定、惯性不足等难题,与新能源一道有着广阔的发展前景。除去考虑技术因素外,储能的长远发展还需要考虑经济性因素,明晰其在系统中的各类价值并与其投资成本相比较。为解决过去文献中储...储能可解决新型电力系统中调峰能力不足、频率不稳定、惯性不足等难题,与新能源一道有着广阔的发展前景。除去考虑技术因素外,储能的长远发展还需要考虑经济性因素,明晰其在系统中的各类价值并与其投资成本相比较。为解决过去文献中储能价值定义不清、核算方式粗糙的问题,提出了一种改进的储能替代性价值测算方法。文章创新性地提出了一种储能替代性价值测算框架,借鉴VCG(vickery clark aloves)机制计算储能的引入对全系统综合成本的降低幅度。在测算综合成本时,运用规划-运行两阶段联合优化模型,考虑源网荷储的优化互动,实现更为准确合理的经济性分析。文章基于IEEE 5节点算例演示了所提方法的效果,并发现储能具有替代发输电投资、降低需求侧响应和备用费用等多元价值。展开更多
Edit distance is an algorithm to measure the difference between two strings,usually represented as the minimum number of editing operations required to transform one string into another.The edit distance algorithm inv...Edit distance is an algorithm to measure the difference between two strings,usually represented as the minimum number of editing operations required to transform one string into another.The edit distance algorithm involves complex dependencies and constraints,making state management and verification work tedious.This paper proposes a derivation and verification method that avoids directly handling dependencies and constraints by proving the equivalence between the edit distance algorithm and existing functional modeling.First,the derivation process of edit distance algorithm mainly includes 1)describing problem specifications,2)inductively deducing recursive relations,3)formally constructing loop invariants using the optimization theory(memorization technology and optimal decision table)and properties(optimal substructure property and subproblems overlapping property)of the edit distance algorithm,4)generating the Minimalistic Imperative Programming Language(IMP)code based on the recursive relations.Second,the problem specification,loop invariants,and generated IMP code are input into Verification Condition Generator(VCG),which automatically generate five verification conditions,and then the correctness of edit distance algorithm is verified in the Isabelle/HOL theorem prover.The method utilizes formal technologies and theorem prover to complete the derivation and verification of the edit distance algorithm,and it can be applied to linear and nonlinear dynamic programming problems.展开更多
文摘储能可解决新型电力系统中调峰能力不足、频率不稳定、惯性不足等难题,与新能源一道有着广阔的发展前景。除去考虑技术因素外,储能的长远发展还需要考虑经济性因素,明晰其在系统中的各类价值并与其投资成本相比较。为解决过去文献中储能价值定义不清、核算方式粗糙的问题,提出了一种改进的储能替代性价值测算方法。文章创新性地提出了一种储能替代性价值测算框架,借鉴VCG(vickery clark aloves)机制计算储能的引入对全系统综合成本的降低幅度。在测算综合成本时,运用规划-运行两阶段联合优化模型,考虑源网荷储的优化互动,实现更为准确合理的经济性分析。文章基于IEEE 5节点算例演示了所提方法的效果,并发现储能具有替代发输电投资、降低需求侧响应和备用费用等多元价值。
基金Supported by the National Natural Science Foundation of China(62462036,62462037)Key Project of Jiangxi Provincial Natural Science Foundation(20242BAB26017)Academic and Major Disciplines in Jiangxi Province Technical Leader Training Project(20232BCJ22013)。
文摘Edit distance is an algorithm to measure the difference between two strings,usually represented as the minimum number of editing operations required to transform one string into another.The edit distance algorithm involves complex dependencies and constraints,making state management and verification work tedious.This paper proposes a derivation and verification method that avoids directly handling dependencies and constraints by proving the equivalence between the edit distance algorithm and existing functional modeling.First,the derivation process of edit distance algorithm mainly includes 1)describing problem specifications,2)inductively deducing recursive relations,3)formally constructing loop invariants using the optimization theory(memorization technology and optimal decision table)and properties(optimal substructure property and subproblems overlapping property)of the edit distance algorithm,4)generating the Minimalistic Imperative Programming Language(IMP)code based on the recursive relations.Second,the problem specification,loop invariants,and generated IMP code are input into Verification Condition Generator(VCG),which automatically generate five verification conditions,and then the correctness of edit distance algorithm is verified in the Isabelle/HOL theorem prover.The method utilizes formal technologies and theorem prover to complete the derivation and verification of the edit distance algorithm,and it can be applied to linear and nonlinear dynamic programming problems.
