High(er) assurance blockchains: functional and performance verification in the software design process 2018-06-06T09:30:12+00:00

Verification Futures 2018

Conference:Verification Futures 2018 (click here to see full programme)
Speaker:Dr Neil Davies, Chief Scientist, Predictable Network Solutions Ltd
Presentation Title:High(er) Assurance Blockchains: Functional and Performance Verification in the Software Design Process
Abstract:The Cardano project is delivering a distributed-ledger proof-of-stake blockchain system as high-assurance software. Central to this assurance is a chain of formal and semi-formal evidence, linking the peer-reviewed blockchain protocol Ouroboros-Praos to deployable Haskell code via a series of refinement steps.

The blockchain protocol relies on distribution of data between nodes of the system with real-time performance criteria that we capture using the ∆Q framework. The design process that we are attempting relies on being able to formally describe versions of the protocol in such a way that we can simulate or execute them, reason formally about relationships between different versions, and do abstract performance evaluations in the ∆Q framework. This enables step by step design refinement, with rapid prototyping, whilst ensuring at each step that we can meet our functional and performance criteria.

This talk will give an overview of this process, the lessons learned and the progress so far towards this ambitious goal.

  • Blockchains are trusted repositories for data having significant value
  • Their security, liveness and utility is tied to their performance
  • Building formal verification directly into the design and development cycle reduces total lifecycle costs
Speaker Bio:Neil Davies is an expert in resolving the practical and theoretical challenges of large scale distributed and high-performance computing, particularly scalability effects in large distributed systems, their operational quality, and how to manage their degradation gracefully under saturation and adverse operational conditions. He is a computer scientist, mathematician and hands-on software developer who builds rigorously engineered working systems and scalable demonstrators of new computing and networking concepts.

Throughout his 20-year career at the University of Bristol he was involved with early developments in networking, its protocols and their implementations. He collaborated with organisations such as NATS, Nuclear Electric, HSE, ST Microelectronics and CERN on issues relating to scalable performance and operational safety. He was also technical lead on several large EU Framework collaborations relating to high performance switching. He has mentored PhD candidates at CERN, and is currently assisting with Ph.D. candidates at the University of Catalonia.

He co-founded Degree2 Innovations in 2000, commercialising network QoS research, and went on to found Predictable Network Solutions in 2003. He has worked on performance aspects of the Department of Defense’s Future Combat Systems project, and has developed approaches to delivering consistent video telephony for sign language users over retail broadband. He is the co-author of several patent families.

T&VS NEWSLETTER SIGN-UP
The T&VS newsletters inform you about industry news, events and information from T&VS. No spam, we promise and it is always easy to unsubscribe.
We never share your information. Read our Privacy Statement
Interested in Formal Verification?
Then why not attend the TVS Formal
Verification Bootcamp training?
The 2-day Formal Verification Bootcamp is for design and verification engineers looking to enhance their knowledge of formal verification and to learn how to write effective assertions to find and fix bugs. The course is a mix of presentations and hands-on development exercises.
Bootcamp Enquiry Form
If you are interested in receiving additional information on the course then simply email Mike Bartley (TVS CEO and Course Leader) by entering your details below.
Interested in SystemC?
FREE SystemC UVM Library Now Available
The TVS SystemC UVM library closely mimics UVM but gives users a license free UVM-based verification environment.
Have your product requirements been successfully tested and implemented?
Find out how asureSIGN can help you implement a successful Requirements Driven Verification and Test Strategy by visiting asureSIGN or enter your details and we will be in touch.
Course Dates and Pricing
To receive additional information, including course dates and pricing, please contact our training team who will be happy to help.
Download Request
Please complete the following form then click 'submit' to access the download.
Presentation Request
Please complete the following form then click 'submit' to gain access to the presentations.
DOWNLOAD REQUEST
Please complete the following form and then click 'submit' to gain access to the download.
FREE QA ASSESSMENTS
Did you get what you were looking?

Let the testing experts help. We will run a FREE QA assessment which will include our top 5 recommendations to help maximise your testing.