what are the advantages and disadvantages of uppaal and spin/promela for modelling embedded systems?
I am a little bit confused - thanks
An outdated paper, but has some useful and relevant points on the comparisons
http://www.brics.dk/RS/96/24/BRICS-RS-96-24.pdf
Design
Considering the design languages, the obvious distinction is the possibility of modelling real–time systems in UPPAAL. In the case study it is shown that interesting bounded liveness properties can be expressed and verified in UPPAAL. Another beneficial feature of UPPAAL is the possibility of committed locations which makes possible a quite natural modelling of the broadcast behaviour needed in the case study. In contrast PROMELA can not apply theatomicity construct on sequences of send- and receive statements as these mightbe blocking
Verification
Considering the verification phase, the kind of properties expressible in the property language of UPPAAL are restricted to invariance and possibility properties. Other properties as e.g. the bounded liveness properties of our case study needs to be expressed as separate test automata probing the design. In section 3.4 we present ideas on how to extend the property language and automatically generate the test automata. This is already possible in SPIN for transforming LTL properties to never automata