Over the course of two days the functional programming community gathered at the largest sector’s event in southern Europe, building bridges between the best of academia and applications in the industrial world.
Alcino Cunha, INESC TEC researcher, was one of the guest speakers at Lamba World – an international conference on functional programming and due applications. As a privileged stage for the meeting of multiple programming languages, the event also allowed the exchange between academia and industry representatives, as well as aficionados.
In his lecture Designing Software with Complex Configurations, Alcino Cunha focused on the design of software with complex configurations using “lightweight” formal methods, namely the TLA + and Alloy languages. The objective was to demonstrate their application in the specification and verification of a simple distributed protocol expected to work in different network configurations.
Formal methods are a powerful mathematical technique in software design. However, many of these methods are quite difficult, with a significant cost. The “lightweight” formal methods are an alternative that favours the use of automatic analysis tools to detect problems in partial specifications of the system to be developed.
The Alloy and TLA+ languages are part of this group, whose application is especially useful in the fast exploration of different design options, but also to ensure that the behaviour of the software meets the expected requirements.
In a workshop entitled Structural Design with Alloy, the INESC TEC researcher also addressed the use of this “lightweight” formal method in terms of software structures design. Based on the motto of the Alloy language – “everything is a relation” – the participants had the opportunity to learn how to model structures through a simple mathematical concept, and how to specify the requirements of said structures through Alloy’s relational logic. Finally, the researcher explained how these formal models can be used to automate the process of testing the implementation of data structures.
Given the more industrial nature of the conference, Alcino Cunha highlighted the “enthusiasm” of the attendees, also highlighting the contacts established soon after towards implementing the shared ideas. “It is a little different from the conferences in which I usually participate, which focus on technical issues. In this case, we approached these questions from a user’s point of view.” According to the researcher, this approach was “quite rewarding”. “It is an excellent way to reach the industry sector,” he concluded.
The researcher mentioned in this news piece is associated with INESC TEC and UMinho.
News, current topics, curiosities and so much more about INESC TEC and its community!
