In the past few years, the focus in microprocessors has shifted from increasing speed to creating processors that contain multiple cores. In order to effectively use the new processors, concurrent specifications and applications must be developed. Additionally, there are many applications that require the specifications to be provably correct. CAPS (Concurrent Automatic Programming System) is designed to aid the user in the creation, execution, and formal verification of concurrent specifications.; The specification language of CAPS (CAPSL) is a very high-level language designed for concurrency and automatic conversion to a colored Petri net (CP-net). For each statement of the language, there exists a mapping to a colored Petri net. Once in the form of a CP-net, the specifications can be formally verified or a simulation can be run.
展开▼
