In PSL, behavioral properties of an IP core and its environment are directed by different directives. Improperly directed properties will severely impact the validity of refinement verification, specification assurance, and the evolution of specification hierarchy. In this paper, we introduce a tool iPSL which supports users to apply IP-based design methodology to PSL specifications. iPSL incorporates three methods for principled construction of PSL specifications. 1) We propose rules which restrict operand types of temporal operators so that we can check whether properties are correctly directed in expressing their roles. 2) We propose semantics for composing IP-based PSL specification. With the semantics, we can pick out properties which need further abstractions after composition. 3) We also provide a semantics for the inherit operator so that we can evolve a system specification from those of existing IP cores.

PSL is a standard specification language(IEEE-1850) for hardware and embedded system design. The simple subset of PSL(PSLSimple) conforms to the notion of monotonic advancement of time, which in turn ensures that formulas within the subset can be simulated easily. Dynamic verifiers consider only finite executions which may be too short to assure their satisfaction to some formulas. In this paper, we work on the theories and methods for designing dynamic verifiers for PSLSimple. We first study the formalism for the formula satisfaction strengths over finite words. Then, we explore the combinational laws of finite words with respect to strong satisfaction, weak satisfaction and strong violation. That contributes acceptance conditions for automata to recognize not just violating, but also strongly satisfying and pending words for all PSLsimplestructures. In the end, we propose the local-variable-enhanced alternating finite automata( LAFA) as the run time checkers for PSLSimple. The size of a LAFA is linear to the size of its PSLSimpleformula.

As a system-level modelling language, SystemC possesses some new and interesting features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we first select a kernel subset of SystemC and study its operational semantics. Based on the operational semantics we define a bisimulation relation, from which program equivalence is explored. Finally, we present a set of algebraic laws for the subset language, which can be proved based on the operational semantics model via bisimulation

Conventional theories of concurrency reduce parallel processes to sequential ones. Here, we propose a true concurrency trace model which takes variables of parallel processes as a whole and runs parallel processes as simultaneous updates on variables. By equipping each resource an ownership variable, the model has a uniform treatment to both variable access conflicts and resource conflicts. A denotational semantics based on the model is studied. After that, we show how to use this model to build a correct resource scheduler, and specify pre-compilers such that the resulting systems do not incur conflicts and have less chance of deadlocks.