Title: Solving the 2015 FMTV Challenge by response time analysis with MAST
Authors: Julio L. Medina, Juan M. Rivas, J. Javier Gutiérrez, and Michael González Harbour (Departamento de Ingeniería Informática y Electrónica, Universidad de Cantabria, Santander, Spain)
Abstract: This paper reports solutions and recommendations regarding the design of the systems proposed in the 2015 edition of the Formal Methods and Timing Verification Challenge (FMTV). It uses the modelling formalism and the schedulability analysis techniques provided by the MAST suite of tools. The paper starts by clarifying the role of the data provided against the design intent. Then, for each of the challenges proposed, it discusses the adequacy of the analysis models used to represent the corresponding timing characteristics as well as the strengths and limitations of the underlying analysis approaches, and presents the results obtained. Finally, we report the effort it took to solve them and the lessons learned. The solutions are also provided in electronic form to facilitate their assessment by the community.
Attached paper:
