Events at MetaForum MF 3

The process algebra TSP extends the process algebra BCCSP with sequential composition and successful termination. For BCCSP it is known, for all semantics in Van Glabbeek’s linear time-branching time spectrum of behavioural semantics, whether a finite basis exists. In this thesis, we study whether these semantics are finitely based over TSP. We discovered that none …continue reading

As technology progresses, newer, and more complex, solutions are employed to verify that rail signalling systems are safe. Formal methods provide ways to increase rigour in the verification process. This precision, accompanied by the ongoing increase of computational power of computers, also opens up ways to partially automate parts of the verification process. We present …continue reading

In mCRL2 numbers are represented using rewrite systems. The representation is based on binary operations. This is relatively concise but far less efficient than 64 bits operations on numbers available in processors. I will explain ongoing work towards an attempt to reap the benefits of processor arithmetic without loosing the advantages of the numbers represented …continue reading

Because of the increase in complexity of System-on-Chip (SoC) networks by using Network-on-Chip (NoC), latency has become a major issue in the design and validation. There are formal and mathematical methods to determine latency bounds of a NoC, such as network calculus, and low level simulation environments, such as a cycle-accurate simulation of the Register …continue reading

Although most model checking logics focus on proving qualitative properties, with the logic plmu*+ introduced in Mio’s PhD thesis one can check the probability that some behaviour happens. In this work we try to bring this logic to practice. We attempt to find intuitive meaning for plmu*+-formulas with the aim to create guidelines to create …continue reading