Abstract
Formal methods constitute a means of developing reliable and correctly behaving software based on a specification. In scenarios where information technology is used as a foundation to enable human communication, this is, however, not always enough. Successful interaction between humans often depends on the concept of trust, which is different from program correctness. In this paper, we present a framework for integrating trust into a formal development process, allowing for the construction of formally correct programs for communication, embracing trust as a central concept. We present a coordination language for use with action systems, taking a modular approach of separating trust aspects from other functionality. We also believe that our work can be adapted to modelling other aspects beside trust. Throughout the paper, we employ a case study as a testbed for our concepts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: assigning programs to meanings. Cambridge University Press, New York, USA (1996)
Back, R.J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: PODC 1983. Proceedings of the second annual ACM symposium on Principles of distributed computing, pp. 131–142. ACM Press, New York, NY, USA (1983)
Back, R.J.R., Sere, K.: Superposition refinement of reactive systems. Formal Aspects of Computing 8(3), 324–346 (1996)
Back, R.J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)
Butler, M., Leuschel, M., Lo Presti, S., Turner, P.: The use of formal methods in the analysis of trust (position paper). In: Jensen, C., Poslad, S., Dimitrakos, T. (eds.) iTrust 2004. LNCS, vol. 2995, pp. 333–339. Springer, Heidelberg (2004)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley Publishing Company, Reading (1988)
Degerlund, F., Sere, K.: A framework for incorporating trust into the action systems formalism (work in progress). In: Aceto, L., Ingólfsdóttir, A. (eds.) NWPT 2006. Proceedings for the 18th Nordic Workshop on Programming Theory, oct 2006, Reykjavík Univerity, Reykjavík, Iceland (2006), abstract
Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Jøsang, A.: Artificial reasoning with subjective logic. In: Proceedings of the 2nd Australian Workshop on Commonsense Reasoning (1997)
Jøsang, A., Hayward, R., Pope, S.: Trust network analysis with subjective logic. In: ACSC 2006. Proceedings of the 29th Australasian Computer Science Conference, pp. 85–94 (2006)
Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Transactions on Programming Languages and Systems 4(3), 382–401 (1982)
Métayer, C., Abrial, J.-R., Voisin, L.: Event-b language, Rodin Deliverable D7. EU-project RODIN (IST-511599) (2005), http://rodin.cs.ncl.ac.uk/deliverables.htm
Neovius, M., Sere, K., Yan, L., Satpathy, M.: A formal model of context-awareness and context-dependency. In: SEFN 2006. Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, pp. 177–185. IEEE Computer Society Press, Los Alamitos (2006)
Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. Journal of the ACM 27(2), 228–234 (1980)
Petre, L., Sere, K., Waldén, M.: A topological approach to distributed computing. In: Proceedings of WDS 1999 - Workshop on Distributed Systems, September 1999. Electronic Notes in Theoretical Computer Science, vol. 28, pp. 97–118. Elsevier, Amsterdam (1999)
Wagealla, W., Carbone, M., English, C., Terzis, S., Lowe, H., Nixon, P.: A formal model for trust lifecycle management. In: FAST 2003. Workshop on Formal Aspects in Security and Trust, pp. 181–192 (2004)
Yan, L., Sere, K.: A formalism for context-aware mobile computing. In: ISPDC 2004. Proceedings of the Third International Symposium on Parallel and Distributed Computing/Third International Workshop on Algorithms, Models and Tools for Parallel Computing on Heterogeneous Networks (ISPDC/HeteroPar’04), Washington, DC, USA, pp. 14–21. IEEE Computer Society Press, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Degerlund, F., Sere, K. (2007). A Framework for Incorporating Trust into Formal Systems Development. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2007. ICTAC 2007. Lecture Notes in Computer Science, vol 4711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75292-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-75292-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75290-5
Online ISBN: 978-3-540-75292-9
eBook Packages: Computer ScienceComputer Science (R0)