|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some research projects currently pursued by members of the AsmCenter
 | | | | | | | | | | | Goal: development of a comprehensive open source tool environment for high-level design, experimental validation and appropriate verifications of abstract system models, starting from a lean language for executable ASMs. Partners: see http://www.coreasm.org/people.php | | | | Mastermind is an interdisciplinary research project in Computational Criminology, a collaborative research initiative by Computing Science and Criminology at SFU, and the RCMP "E" Division. The goal of Mastermind is to provide criminologists with innovative computational methods and supporting tools for studying crime. Arguably, the use of advanced computer models in crime analysis and decision support leads to novel strategies for urban planning, policy making and crime reduction/ prevention. By combining the Abstract State Machine formalism with the multi-agent modeling paradigm, we obtain a formal semantic framework for modeling and integration of established theories of crime. Mastermind specifically focuses on spatiotemporal aspects of crime in urban areas. This project is partially funded by MITACS ( http://www.mitacs.ca) and the RCMP "E" Devision ( http://www.rcmp-grc.gc.ca/bc/home/index_e.htm). | | | | Security of civil aviation has become a major concern in recent years, especially due to the increasing number of potential and real threats imposing dynamically changing risks on airport and aircraft security. Safeguard is a project aiming at computational analysis, validation and verification of aviation security requirements. Within the Safeguard project a novel computational framework for machine-assisted inspection of the efficiency and effectiveness of procedural security measures is being developed. To cope with the inherent uncertainty of security systems, probabilistic modeling methods are combined with probabilistic model checking techniques. Specifically, Abstract State Machines and Probabilistic Timed Automata are used together with the PRISM model checker. This project is partially funded by MITACS ( http://www.mitacs.ca) and the RCMP "E" Devision ( http://www.rcmp-grc.gc.ca/bc/home/index_e.htm). | | | | The TASM Language was developed at the Embedded Systems Laboratory of MIT (Cambridge/MA, USA) as an extension to the Abstract State Machine (ASM) Language. The core idea behind the TASM language is to incorporate functional and non-functional properties into a single specification language. Most specifically, the TASM language can specify functional behavior, timing behavior, and resource consumption. Through the TASM language, it is possible to develop literate, reusable, executable, and verifiable embedded real-time system specifications. The associated TASM Toolset implements the language features and provides a set of functionality to support the engineering of embedded real-time systems across lifecycle phases. |
|
|
|
|
|
|
 |
|
|
|
|