Our aim is a specification language and a refinement concept which covers the whole development process of real-time systems. This includes the description of requirements and design decisions, down to algorithms. In the tradition of Dynamic Logic, processes become explicit in our approach. Thus, the task of proving monomorphicity can be dealt with using the KIV system. Here, the KIV system takes a particular position since it supports dynamic logic which has been proved useful in specification of knowledge-based systems.
Several improvements are under work.
Please feel free to ask for further informations. These references are also available as a BibTex file. Further references can be found at the KIV home page at Augsburg . Specification and Verification of Knowledge-Based Systems . Using KIV to Specify and Verify Architectures of Knowledge-Based Systems .