Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types
Concrete artefacts are produced and used for dissemination. These include scientific publications, a repository of use-cases, tutorials, a non-technical article presenting the main achievements of the project, material for tutorials and recorded tutorials. These artefacts will remain available to the general public beyond the duration of the project and promote a continuative and long-term dissemination.
If you are unable to view these files, please log in or register.
We identify two important features to enhance the design of communication protocols specified in the pi-calculus, that are linear and static channels, and present a compiler, named GoPi, that maps high level specifications into executable Go programs. Channels declared as linear are deadlock-free, while the scope of static channels, which are bound by a hide declaration, does not enlarge at runtime; this is enforced statically by means of type inference, while specifications do not include annotations. Well-behaved processes are transformed into Go code that supports non-deterministic synchronizations and race-freedom. We sketch two main examples involving protection against message forwarding, and forward secrecy, and discuss the features of the tool, and the generated code. We argue that GoPi can support academic activities involving process algebras and formal models, which range from the analysis and testing of concurrent processes for research purposes to teaching formal languages and concurrent systems.
Petri Nets are a well-known model of concurrency and pro- vide an ideal setting for the study of fundamental aspects in concurrent systems. Despite their simplicity, they still lack a
Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is stan- dard for multiparty session type systems
Abstract: OpenDXL is an open API to enable devices to share intelligence and orchestrate security operations in real-time. This security connected platform from McAfee provides a unified framework for hundreds
Abstract: Regulatory compliance describes the level of alignment between business processes and legislations, and it represents a complex process where regulations have to be instantiated in terms of a business
Abstract: In the manufacturing industry downtime is very expensive, therefore most small and midsize factories are still managed using paper-based processes. The problem space is perfectly suited for a microservices
Abstract: Effectively exchanging and acting upon threat intelligence in a diverse, heterogeneous landscape such as cyber security has proven an elusive goal. With the continuous evolution of both the security