RefineNet

Refine 2019

Co-located with FM 2019 (Porto, October 2019). New Register here! New Schedule is available here. Call for papers. Selected papers of the proceedings will be published as an LNCS volume. Paper submission (extended): July 15, 2019 Notification (extended): Aug 9, 2019 Proceedings version ready: Sept 2, 2019 Workshop: October 7, 2019

This is the RefineNet home page.

RefineNet was an EPSRC-funded network in the area of refinement of formal specifications (2004-2007), and is now a special interest group of BCS-FACS.

Work on the foundations of languages such as Z, B, VDM and CSP have led to their widespread use in certain industrial sectors, e.g., those with security or safety critical concerns. In addition to precise specification, formal methods also allow the possibility of precise and verifiable development, as captured by the concept of refinement.

Refinement is one of the cornerstones of a formal approach to software engineering. Refinement is the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification.

Work on refinement in the late 80s made initial progress in a number of areas, however recently new aspects of the subject have been explored. This has been inspired by a number of factors including new applications, industrial case studies, integration of notations and the need for proper tool support. The subject has therefore moved from initial work conducted in individual notations to a more wide ranging focus.

The purpose of RefineNet was to bring together people who are interested in the development of concrete designs or executable programs from formal specifications, tool support for formal software development, and those who have practical experience with formal refinement methodologies.

The network focused around problems in two strands, industrial and foundational:

Industrial

• How best can the refinement process be automated?
• How can smaller scale refinement techniques be scaled up?
• How can current industrial practice and experience be progressed in this area?

Foundational

• How is refinement best supported in integrated notations (both informal and formal)?
• What foundations and generalisations are needed?
• What are the appropriate compositional refinement techniques?
• What theory and practice is needed for refinement in OO languages, including UML?
• How can aspects of concurrency and distribution be best supported?

The network was structured around a series of workshops as follows:

• A series of informal research meetings held quarterly.
• A series of Refinement workshops held once a year, providing the focal point for dissemination of results and interaction with all those interested in refinement.