Abstract
A Run-Time Management system for many-core architecture is aware of application requirements and able to save energy by sacrificing performance when it will have negligible impact on user experience. This paper outlines the application of a process for development of a run-time management system that integrates a range of modelling, validation, verification and generation tools at appropriate stages. We outline the models, process and tools we used to develop a temperature aware run-time management system for Dynamic Voltage and Frequency Scaling (DVFS) of a media display application. The Event Refinement Structure (ERS) approach is used to visualise the abstract level of the DVFS control. The Model Decomposition technique is used to tackle the complexity of the model. To model the process-oriented aspects of the system we used iUML-B Statemachines. We use several different visual animation tools, running them synchronously to exploit their different strengths, in order to demonstrate the model to stakeholders. In addition, a continuous model of the physical properties of the cores is simulated in conjunction with discrete simulation of the Event-B run-time management system. Finally executable code is generated automatically using the Code Generation plug-in. The main contribution of this paper is to demonstrate the complementarity of the tools and the ease of their integrated use through the Rodin platform.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Oboril, F., Tahoori, M.: Extratime: Modeling and analysis of wearout due to transistor aging at microarchitecture-level. In: 2012 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 1–12 (June 2012)
PRiME: Power-efficient, Reliable, Many-core Embedded systems, http://www.prime-project.org
Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer 12(6), 447–466 (2010)
Yeganefard, S., Butler, M.: Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation. ECEASST 46 (2011)
Yeganefard, S., Butler, M.: Control Systems: Phenomena and Structuring Functional Requirement Documents. In: ICECCS, pp. 39–48 (2012)
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Salehi Fathabadi, A., Butler, M., Rezazadeh, A.: A Systematic Approach to Atomicity Decomposition in Event-B. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 78–93. Springer, Heidelberg (2012)
Snook, C.: Modelling Control Process and Control Mode with Synchronising Orthogonal Statemachines. In: B2011. Limerick (2011)
Savicks, V., Snook, C.: A Framework for Diagrammatic Modelling Extensions in Rodin. In: Rodin Workshop 2012, Fontainbleau (2012)
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B Models with B-Motion Studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009)
Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition tool for Event-B. Softw., Pract. Exper. 41(2), 199–208 (2011)
Hoang, T.S., Iliasov, A., Silva, R., Wei, W.: A Survey on Event-B Decomposition. ECEASST 46 (2011)
Savicks, V., Butler, M., Bendisposto, J., Colley, J.: Co-simulation of Event-B and Continuous Models in Rodin. In: Rodin Workshop 2013, Turku (2012)
Edmunds, A., Butler, M.: Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In: PLACES (2011)
Butler, M., Maamria, I.: Practical Theory Extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67–81. Springer, Heidelberg (2013)
Fritzson, P., Engelson, V.: ModelicaA unified object-oriented language for system modeling and simulation. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 67–90. Springer, Heidelberg (1998)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
ADVANCE: Advanced Design and Verification Environment for Cyber-physical System Engineering, http://www.advance-ict.eu/
Ge, Y., Qiu, Q.: Dynamic thermal management for multimedia applications using machine learning. In: DAC, pp. 95–100 (2011)
Parnas, D.L., Madey, J.: Functional Documents for Computer Systems. Science of Computer Programming 25, 41–61 (1995)
Abrial, J.R.: The B-book - assigning programs to meanings. Cambridge University Press (2005)
Back, R.J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)
Dghaym, D., Butler, M., Fathabadi, A.S.: Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling. ECEASST 66 (2013)
Back, R.J.: Refinement calculus, part ii: Parallel and reactive programs. In: REX Workshop, pp. 67–93 (1989)
Abrial, J.-R., Su, W., Zhu, H.: Formalizing Hybrid Systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012)
Edmunds, A., Butler, M., Maamria, I., Silva, R., Lovell, C.: Event-B Code Generation: Type Extension with Theories. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 365–368. Springer, Heidelberg (2012)
Fraser, M.D., Kumar, K., Vaishnavi, V.K.: Strategies for incorporating formal specifications in software development. Commun. ACM 37(10), 74–86 (1994)
Kemmerer, R.: Integrating formal methods into the development process. IEEE Software 7(5), 37–50 (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Salehi Fathabadi, A., Snook, C., Butler, M. (2014). Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)