2016/05/16 by Ashish Darbari, Iain Singleton, Darbari, Ashish +5
Computer Science · #Advanced Software Engineering Methodologies #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Real-Time Systems Scheduling #Software Engineering (cs.SE) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1605.04744
openalex publication_date 2016/05/16 · openalex created_date 2022/10/01 · openalex updated_date 2026/07/28
The HSA Foundation has produced the HSA Platform System Architecture\nSpecification that goes a long way towards addressing the need for a clear and\nconsistent method for specifying weakly consistent memory. HSA is specified in\na natural language which makes it open to multiple ambiguous interpretations\nand could render bugs in implementations of it in hardware and software. In\nthis paper we present a formal model of HSA which can be used in the\ndevelopment and verification of both concurrent software applications as well\nas in the development and verification of the HSA-compliant platform itself. We\nuse the Event-B language to build a provably correct hierarchy of models from\nthe most abstract to a detailed refinement of HSA close to implementation\nlevel. Our memory models are general in that they represent an arbitrary number\nof masters, programs and instruction interleavings. We reason about such\ngeneral models using refinements. Using Rodin tool we are able to model and\nverify an entire hierarchy of models using proofs to establish that each\nrefinement is correct. We define an automated validation method that allows us\nto test baseline compliance of the model against a suite of published HSA\nlitmus tests. Once we complete model validation we develop a coverage driven\nmethod to extract a richer set of tests from the Event-B model and a user\nspecified coverage model. These tests are used for extensive regression testing\nof hardware and software systems. Our method of refinement based formal\nmodelling, baseline compliance testing of the model and coverage driven test\nextraction using the single language of Event-B is a new way to address a key\nchallenge facing the design and verification of multi-core systems.\n