Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Software and Systems Modeling
Published in: Software and Systems Modeling 4/2016

15-03-2015 | Theme Section Paper

The Unit-B method: refinement guided by progress concerns

Authors: Simon Hudon, Thai Son Hoang, Jonathan S. Ostroff

Published in: Software and Systems Modeling | Issue 4/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.
previous article Constructing and verifying a robust Mix Net using CSP
next article Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
In this paper, we use \(f.x\) to denote the result of applying a function \(f\) to argument \(x\). Function application is left-associative, so \(f.x.y\) is the same as \((f.x).y\).
 
2
\(loc{\vartriangleleft \!\!\!\!-}\{t\mapsto Exit\}\) denotes a relation equal to \(loc\) excepts for the entry for \(t\) which is mapped to \(Exit\).
 
Literature
1.
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefMATH
2.
Abrial, J.R.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
3.
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)CrossRef
4.
Chandy, M., Misra, J.: Parallel program design - a foundation. Addison-Wesley, Reading (1989)MATH
5.
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
6.
Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, New York (1990)CrossRefMATH
7.
8.
9.
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Boehm, BW., Garlan, D., Kramer, J. (eds.) ICSE’ 99, pp. 411–420. ACM, Los Angeles, CA, USA (1999)
10.
11.
Hoang, T., Abrial, J.R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM, LNCS, vol. 6991, pp. 456–471. Springer, Berlin (2011)
12.
Hudon, S.: A progress preserving refinement. Master’s thesis. ETH Zurich (2011)
13.
Hudon, S., Hoang, T.: Development of control systems guided by models of their environment. ENTCS 280, 57–68 (2011)
14.
Hudon, S., Hoang, T.: Systems design guided by progress concerns. In: Johnsen, EB., Petre, L. (eds.) Proceedings of the 10th International Conference on Integrated Formal Methods (IFM2013), Turku, Finland, June 2013. Integrated Formal Methods. Lecture Notes in Computer Science, vol 7940, pp. 16–30. Springer (2013)
15.
Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1986)
16.
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)
17.
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRef
18.
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)
19.
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Response. In: Manna, Z., Peled, D. (eds.) Time for Verification, Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science, vol. 6200, pp. 279–361. Springer, Berlin (2010)
20.
21.
Méry, D., Poppleton, M.: Formal modelling and verification of population protocols. In: Johnsen, E.B., Petre, L. (eds.) IFM, Lecture Notes in Computer Science, vol. 7940, pp. 208–222. Springer, Berlin (2013)
22.
Spivey, J.M.: Z Notation—A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
Metadata
Title
The Unit-B method: refinement guided by progress concerns
Authors
Simon Hudon
Thai Son Hoang
Jonathan S. Ostroff
Publication date
15-03-2015
Publisher
Springer Berlin Heidelberg
Published in
Software and Systems Modeling / Issue 4/2016
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-015-0456-2

Other articles of this Issue 4/2016

Software and Systems Modeling 4/2016 Go to the issue

Guest Editorial

Theme issue on Integrated Formal Methods

Theme Section Paper

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Theme Section Paper

A framework for deadlock detection in core ABS

Theme Section Paper

Contract-based verification of discrete-time multi-rate Simulink models

Regular Paper

Supporting different process views through a Shared Process Model

Theme Section Paper

Model-checking software library API usage rules

Premium Partner

    Image Credits