Jiale Zhou
Jiale Zhou is a Ph.D. student at Mälardalen University (MDH) since February 2011. He got a Bachelor Degree in Electronic Engineering at Shanghai Jiao Tong University (SJTU), China, in 2007. Jiale Zhou received a M.Sc. in Computer Science at MDH, in October 2010. During his master study, he stayed in Eindhoven University of Technology (TU/e), Holland, for half a year as an exchange student. His MSc Thesis project is “Telecom and Internet Services Mashup in Robotics - Design, Architecture and Prototyping”. He is now working together with Prof. Kristina Lundqvist on a project focusing on Software Traceability at Mälardalen Real-Time Research Centre (MRTC).
Research description: Software development processes undergo numerous phases until a final product is reached, each of them generating one or several artifacts. Together, the artifacts describe and constraint the entire system from the different levels of abstraction necessary to bring forth a final product conforming to the requirements. These requirements are commonly decomposed and modified through the artifacts down to the final product. This results in a complex and unmanageable environment to verify each artifact towards their specified constraints. The aim of the research is to develop a holistic framework supporting various specification, design and implementation languages used in the architecture design phase all the way to the implementation phase, where each corresponding artifact is automatically verified against its specified constraints. As a result, the framework can be used to automatically check the consistency and completeness among artifacts generated from different phases in the development process. The research goal faces two overarching challenges, 1) automated verification demands formal traceability among the various artifacts, and 2) consistency and completeness checking among diverse artifacts demands a versatile language to implement the verification techniques. We propose traceability through a common formal language – Timed Abstract State Machines (TASM) – to formally specify the different languages’ semantics, and thereby having a common underpinning providing the traceability. Moreover, TASM provides model-checking and model-based testing features which enables implementation of developed verification techniques.
Research description: Software development processes undergo numerous phases until a final product is reached, each of them generating one or several artifacts. Together, the artifacts describe and constraint the entire system from the different levels of abstraction necessary to bring forth a final product conforming to the requirements. These requirements are commonly decomposed and modified through the artifacts down to the final product. This results in a complex and unmanageable environment to verify each artifact towards their specified constraints. The aim of the research is to develop a holistic framework supporting various specification, design and implementation languages used in the architecture design phase all the way to the implementation phase, where each corresponding artifact is automatically verified against its specified constraints. As a result, the framework can be used to automatically check the consistency and completeness among artifacts generated from different phases in the development process. The research goal faces two overarching challenges, 1) automated verification demands formal traceability among the various artifacts, and 2) consistency and completeness checking among diverse artifacts demands a versatile language to implement the verification techniques. We propose traceability through a common formal language – Timed Abstract State Machines (TASM) – to formally specify the different languages’ semantics, and thereby having a common underpinning providing the traceability. Moreover, TASM provides model-checking and model-based testing features which enables implementation of developed verification techniques.