TY - GEN

T1 - Analysis of a mixed-signal circuit in hybrid process algebra ACP hssrt

AU - Man, K. L.

AU - Schellekens, M. P.

PY - 2007

Y1 - 2007

N2 - ACPhssrt is a hybrid process algebra obtained by extending a combination of two existing extensions of Algebra of Communicating Processes (ACP), namely the process algebra with continuous relative timing and the process algebra with propositional signals, for the specification and analysis of hybrid systems. In addition to equational axioms, this hybrid process algebra has rules to derive equations with the help of real analysis. ACPhssrt is also closely related to the theory of hybrid automata, so ACPhssrt can be reasonable easily translated to hybrid automata. This enables automatic verification of ACPhs srt specifications using existing hybrid automaton-based verification tools (e.g. PHAVer and HyTech). Since ACPhssrt' is a well-developed algebraic theory from the field of hybrid process algebras with the above-mentioned features, it seems to allow rigorous specification and analysis of digital/analog/mixed-signal circuits. In order to explore this fact, in this paper, we study a mixed-signal circuit: a half wave rectifier in ACPhssrt. Some basic properties of the half wave rectifier are analysed in a formal way and some correctness requirements are also proven to be satisfied.

AB - ACPhssrt is a hybrid process algebra obtained by extending a combination of two existing extensions of Algebra of Communicating Processes (ACP), namely the process algebra with continuous relative timing and the process algebra with propositional signals, for the specification and analysis of hybrid systems. In addition to equational axioms, this hybrid process algebra has rules to derive equations with the help of real analysis. ACPhssrt is also closely related to the theory of hybrid automata, so ACPhssrt can be reasonable easily translated to hybrid automata. This enables automatic verification of ACPhs srt specifications using existing hybrid automaton-based verification tools (e.g. PHAVer and HyTech). Since ACPhssrt' is a well-developed algebraic theory from the field of hybrid process algebras with the above-mentioned features, it seems to allow rigorous specification and analysis of digital/analog/mixed-signal circuits. In order to explore this fact, in this paper, we study a mixed-signal circuit: a half wave rectifier in ACPhssrt. Some basic properties of the half wave rectifier are analysed in a formal way and some correctness requirements are also proven to be satisfied.

KW - Digital/analog/mixed-signal circuits

KW - Formal analysis

KW - Formal languages

KW - Formal semantics

KW - Hybrid process algebras

UR - http://www.scopus.com/inward/record.url?scp=84888385492&partnerID=8YFLogxK

M3 - Conference Proceeding

AN - SCOPUS:84888385492

SN - 9789889867140

T3 - Lecture Notes in Engineering and Computer Science

SP - 568

EP - 573

BT - IMECS 2007 - International MultiConference of Engineers and Computer Scientists 2007

T2 - International MultiConference of Engineers and Computer Scientists 2007, IMECS 2007

Y2 - 21 March 2007 through 23 March 2007

ER -