[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Mixing TLA+ and SOS

Hi there,

Structural operational semantics (SOS) [1] is a formal method to specify the semantics of a programming language esp. at runtime
using transition systems for program state. 

Suppose that for programming language L, there exists an SOS spec. One of the main features of L is concurrency.
I am wondering and curious if TLA+ can be used to specify such a programming language, and thus the runtime 
that a running programming in L would create. The goal is to be able to prove/disprove certain properties of the runtime
of the language in regards with concurrency, such as dead locks or live locks.

I am very new to TLA so excuses if the question lacks certain prerequisites.


[1]: https://www.alice.virginia.edu/~weimer/2006-655/reading/plotkin81structural.pdf