Publications

Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for synchronous communication model. We transform the partitioning into a reachability problem in timed automata. By means of an optimal reachability algorithm, an optimal result can be obtained in terms of limited resources in hardware. To increase the opportunity of partitioning optimization, two algorithms are designed to explore the dependency relation among processes in the initial specification. Moreover, we propose a scheduling algorithm to improve the synchronous communication efficiency further after partitioning stage. Some experiments are conducted with model checker UPPAAL to show our approach is both effective and efficient.

 Proceedings of the 1st International Workshop on Harnessing Theories for Tool Support in Software TTSS'07, 22-23 September 2007, Macau SAR, China

Web navigation model provides a dynamic view for web modelling. It is useful for clarifying requirements and specifying implementation behaviors of systems from design intensions. In this paper, we propose a formal model to describe web navigation of user behaviors, where link activities play an important role. Several issues have been considered in our model, such as web browser effects, adaptive navigation, frame communication etc. After the link activity model is established, we use model checker SPIN to check whether there exist problems such as such as broken links, dead ends, missed reply pages, reachability of pages etc. This method can help us to analyze user behaviors, meanwhile it provides us a way to expose design faults in web systems.