Ett ramverk för parallelprogrameringsspecifikationer
Tidsperiod: 2015-01-01 till 2018-12-31
Projektledare: Joachim Parrow
Budget: 3 600 000 SEK
This project is a direct continuation of the project "A framework for parallel programming models", to accommodate and verify a spectrum of high-level modeling languages. We formally established correctness in a theorem prover, and provided an accompanying prototype analysis tool. As a result we unified many existing high-level modeling formalisms, and corrected errors in several several of them. We have also shown how to construct new such formalisms in a systematic way. Now we shall extend this framework to make it easier to apply, and include important elements motivated by realistic applications. We shall include specification languages such as modal logics and modal transition systems, and consider the accompanying problems of model checking and refinement checking. We shall address non-functional aspects such as resource usage, time consumption, and probabilistic behavior. We intend to support a user to define a domain specific formalism, by providing off-the shelf components and ways to combine them. We shall continue our pioneering work with the theorem prover and tie it more closely to the prototype analysis tool. Theory and tools will be developed in parallel with significant applications to guide both.