期刊文献+

基于混合自动机的PSL模型研究 被引量:2

Research on extending PSL model with hybrid automata
下载PDF
导出
摘要 基于SPICE的计算机仿真方法在混合信号电路验证应用中具有较大的计算开销,讨论基于属性描述的建模方法减小计算开销的问题。通过分析PSL(property specification language)对系统属性的形式化描述方法,并分析混合自动机理论对混合信号系统抽象能力,提出了适合于混合信号电路系统快速验证的PSL模型。结合混合自动机对PSL进行了基于混合自动机语义特点的扩展,使用巴克斯—诺尔范式对其拓展后语法进行规范,提出具有描述混合信号电路行为特性的HAPSL(hybrid automata-based PSL),并针对参考电路的混合信号特性进行了分析,详细说明了HAPSL模型描述在混合信号验证中的实现方法和意义。通过与SPICE仿真器对相同电路进行比较仿真实验,显示HAPSL方法数据在适当规模混合信号电路瞬态分析以及状态分析中具有较高的效率并且具有可接受的精确度。 SPICE based simulation in analog and mixed-signal system (AMS) needs lot of computing sources and spends lot of computing time. This paper presented a property specified method for modefing to reduce computation. This paper addressed the formal method for modeling and verification of AMS with hybrid automata based PSL (property specification language ). And presented the theoretical foundation of abstracting AMS with hybrid automata to derive PSL model extended to AMS verification. This paper presented a novel methodology HAPSL(hybrid automata-based PSL) ,which the syntax was defined by EBNF. The continued and temporal property of mixed signal circuit could be abstracted and modeled by using HAPSL. To illustrate this method, provided the analysis of a sample oscillator circuit with HAPSL in the end. Comparing with SPICE, HAPSL is more efficiency and the accuracy is acceptable in mixed-signal circuit.
出处 《计算机应用研究》 CSCD 北大核心 2010年第1期196-199,203,共5页 Application Research of Computers
关键词 计算机仿真 混合自动机 混合信号电路 模型 形式化方法 computer simulation hybrid automata mixed-signal circuit model formal method
  • 相关文献

参考文献9

二级参考文献38

  • 1杜慧敏,曾泽沧,孟李林,韩俊刚,沈绪榜.建立SDH系列芯片验证平台[J].计算机辅助设计与图形学学报,2004,16(5):678-681. 被引量:5
  • 2薛乐,魏晨,陈宗基.混合系统的建模设计与仿真综述[J].计算机仿真,2006,23(6):1-5. 被引量:2
  • 3郑大钟 赵千川.离散事件动态系统[M].清华大学出版社,1999.. 被引量:7
  • 4R Alur,T A Henzinger and P H Ho.Automatic Symbolic Verification of Embedded Systems[J].IEEE Transactions on Software Engineering,1996,22:181-201. 被引量:1
  • 5Johan Bengtsson,Palle Christensen,Per Jensen,Kim G Larsen,Fredrik Larsson,Paul Pettersson,Thomas S rensen and Wang Yi.Uppaal:a Tool Suite for Validation and Verification of Real-Time Systems[M].User guide,1996. 被引量:1
  • 6M Johansson and A Rantzer.Computation of piecewise quadratic Lyapunov function for hybrid systems[J].IEEE Trans.On Automatic Control,1998,34(4):555 -559. 被引量:1
  • 7K X He and M D Lemon.Lyapunov stability of continuous -valued systems under the supervision of discrete-event transition systems[M].Hybrid Systems:Computation and Control (HSCC'98).Berlin,Germany:Springer-Verlag,1998.175-189. 被引量:1
  • 8Hong Seong Park,Young Sin Kim and Wook Hyun Kwon.Model and Stability of Hybrid Systems[M].DIMACS workshop on Verification and Control of Hybrid Systems,1995-10. 被引量:1
  • 9Raymond A DeCarlo,Michael S Branicky,Stefan Pettersson.Perspectives and results on the stability and stabilizability of hybrid systems[C].Proceedings of the IEEE,2000,88(7):1069-1082. 被引量:1
  • 10C Tomlin,J Lygeros,S Sastry.A game theoretic approach to controller design for hybrid systems[C].Proceedings of the IEEE,July 2000. 被引量:1

共引文献5

同被引文献21

引证文献2

二级引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部