Abstract
Salt is a general purpose specification and assertion language developed for creating concise temporal specifications to be used in industrial verification environments. It incorporates ideas of existing approaches, such as PSL or Specification Patterns, in that it provides operators to express scopes and exceptions, as well as support for a subset of regular expressions. On the one hand side, Salt exceeds specific features of these approaches, for example, in that it allows the nesting of scopes and supports the specification of real-time properties. On the other hand, Salt is fully translatable to LTL, if no real-time operators are used, and to TLTL (also known as state-clock logic), if real-time operators appear in a specification. The latter is needed in particular for verification tasks to do with reactive systems imposing strict execution times and deadlines. Salt’s semantics is defined in terms of a translation to temporal (real-time) logic, and a compiler is freely available from the project web site, including an interactive web interface to test drive the compiler. This tutorial paper details on the theoretical foundations of Salt as well as its practical use in applications such as model checking and runtime verification.
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.
Similar content being viewed by others
References
Bauer, A., Leucker, M., Streit, J.: SALT—Structured Assertion Language for Temporal Logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 757–775. Springer, Heidelberg (2006)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symposium on the Foundations of Computer Science (FOCS), Providence, Rhode Island, pp. 46–57. IEEE, Los Alamitos (1977)
Raskin, J.-F., Schobbens, P.-Y.: State clock logic: A decidable real-time logic. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 33–47. Springer, Heidelberg (1997)
D’Souza, D.: A logical characterisation of event clock automata. International Journal of Foundations of Computer Science 14(4), 625–639 (2003)
Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles (1968)
McMillan, K.L.: The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)
Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering 23, 279–295 (1997)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. 21st Int. Conf. on Software Engineering (ICSE), pp. 411–420. IEEE, Los Alamitos (1999)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd Int. Conf. on Software Engineering (ICSE), IEEE, Los Alamitos (2000)
Accellera Property Specification Language. Reference Manual 1.1 (April 2004)
Eisner, C., Fisman, D.: A Practical Introduction to PSL (Series on Integrated Circuits and Systems). Springer, Heidelberg (2006)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 163–173. ACM, New York (1980)
Markey, N.: Temporal logic with past is exponentially more succinct, concurrency column. Bulletin of the EATCS 79, 122–128 (2003)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Proc. Conference on Logic of Programs, pp. 196–218. Springer, Heidelberg (1985)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Heidelberg (1995)
Fix, L.: Fifteen years of formal property verification in intel. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking, pp. 139–144. Springer, Heidelberg (2008)
Ashenden, P.J.: The Designer’s Guide to VHDL, 2nd edn. Morgan Kaufmann Publishers Inc., San Francisco (2001)
Ferro, L., Pierre, L.: Formal semantics for PSL modeling layer and application to the verification of transactional models. In: Proc. Conference on Design, Automation and Test in Europe (DATE), pp. 1207–1212. European Design and Automation Association (2010)
Corbett, J.C., Dwyer, M., Hatcliff, J., Robby: A language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885. Springer, Heidelberg (2000)
Corbett, J., Dwyer, M., Hatcliff, J., Robby: Expressing checkable properties of dynamic systems: The Bandera specification language. Technical Report 04, Kansas State University, Department of Computing and Information Sciences (2001)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)
Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. Aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The forSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)
Eisner, C.: PSL for Runtime Verification: Theory and Practice. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 1–8. Springer, Heidelberg (2007)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Fifth International Conference on Verification, Model Checking and Abstract Interpretation (2004)
ChaoChen, Z., Hoare, T., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Bradfield, J., Stevens, P.: Observational mu calculus. In: Proc. Workshop on Fixed Points in Computer Science (FICS), pp. 25–27 (1998); An extended version is available as BRICS-RS-99-5
Bradfield, J.C., Filipe, J.K., Stevens, P.: Enriching OCL using observational mu-calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 203–217. Springer, Heidelberg (2002)
Lange, M.: Linear time logics around psl: Complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 90–104. Springer, Heidelberg (2007)
Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Technical report, Stanford, CA, USA (1990)
Fritz, C.: Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)
Gastin, P., Oddoux, D.: Fast LTL to büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Leucker, M., Sánchez, C.: Regular Linear Temporal Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291–305. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bauer, A., Leucker, M. (2011). The Theory and Practice of SALT. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)