In this work we investigate some issues in applying formal methods to hybrid system development and develop a categorical framework. We study the themes of stochastic reasoning, heterogeneous formal specification and retrenchment. Hybrid systems raise a rich pallets of aspects that need to be investigated, but never the issue of how the multitude of logics, methodologies and tools can be used altogether. We attack this very difficult issue using categorical logic. When applying formal methods hybrid systems, new (formal methods) mathematics can be created. In this sense, we present new developments in categorical logic, inspired by the control engineering way of treating different aspects of systems. As stochastic reasoning has recently seized its importance in modelling and analysing hybrid systems, we present a uniform categorical formalisation of discrete, continuous and stochastic hybrid systems. A categorical, semantic framework is developed in order to help relating different aspects of hybrid system development.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||26|
|Publication status||Published - 18 Mar 2008|
|Name||CTIT Technical Report Series|
|Publisher||Centre for Telematics and Information Technology, University of Twente|
Bujorianu, M. C., & Bujorianu, L. M. (2008). Formal Engineering Hybrid Systems: Semantic Underpinnings. (CTIT Technical Report Series; No. TR-CTIT-08-28). Enschede: Centre for Telematics and Information Technology (CTIT).