Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment (FM 2026 - ABZ)

Who

Sean McLaren, Tsutomu Kobayashi, Leon Wong, Paul Harvey

Track

FM 2026 ABZ

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 19 May 2026 11:25 - 11:50 at 2F Conf Room 4 - ABZ Session 1: Concurrent and Distributed Systems Chair(s): Dominique Mery

Sean McLaren

University of Glasgow

United Kingdom

Tsutomu Kobayashi

Japan Aerospace Exploration Agency (JAXA)

Japan

Leon Wong

Rakuten Mobile, Inc

Japan

Paul Harvey

Rakuten Mobile Innovation Studio

Japan

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Tue 19 May
Displayed time zone: Osaka, Sapporo, Tokyo change

11:00 - 12:30	ABZ Session 1: Concurrent and Distributed SystemsABZ at 2F Conf Room 4 Chair(s): Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France

11:00 25m Talk		Identifying Design Flaws in a Lock-Free Task Pool with TLA+ ABZ Ilya Shchepetkov Kaspersky Lab, Vasil Dyadov Kaspersky Lab, Alexander Kogtenkov Kaspersky Lab
11:25 25m Talk		Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment ABZ Sean McLaren University of Glasgow, Tsutomu Kobayashi Japan Aerospace Exploration Agency (JAXA), Leon Wong Rakuten Mobile, Inc, Paul Harvey Rakuten Mobile Innovation Studio
11:50 25m Talk		Formal Verification of Healthcare Computer Network Architectures using Alloy and TLA+ ABZ Daniel Daukševič Institute of Computer Science, Vilnius University, Vilnius,Lithuania, Linas Laibinis Institute of Computer Science, Vilnius University, Vilnius,Lithuania
12:15 15m Talk		Formal Verification of Decentralized Autonomous Organizations ABZ Simone Valentini University of Milan, Sowelu Avanzo University of Turin, Elvinia Riccobene Computer Science Dept., University of Milan