 Well-behaved scalable systems are characterised by those systems, which fulfil such a kind of property if already one prototype system (depending on the property) fulfils that property. |
A formal framework provides construction principles for well-behaved scalable systems, such that starting with a prototype system satisfying a desired safety property result in a scalable system satisfying a corresponding safety property, To this end, construction principles for well-behaved scalable systems are design principles for verifiability. With respect to different aspects of scalability, the focus of this work is on property preserving structural scalability. Sufficient conditions to specify a certain kind of basic well-behaved scalable systems are given and it is shown, how to construct more complex systems by the composition of several synchronisation conditions. Scalable safety properties can be used to express privacy policies as well as security and dependability requirements. The parameterised problem of verifying such a property is reduced to a finite state problem for well-behaved scalable systems. |
| Peter Ochsenschläger and Roland Rieke (2015), Pairs of Languages Closed under Shuffle Projection, arXiv 1503.08602. [Abstract] [BibTeX] [Paper (free access)] [Author's version] |
| Abstract: Shuffle projection is motivated by the verification of safety properties of special parameterized systems. Basic definitions and properties, especially related to alphabetic homomorphisms, are presented. The relation between iterated shuffle products and shuffle projections is shown. A special class of multi-counter automata is introduced, to formulate shuffle projection in terms of computations of these automata represented by transductions. This reformulation of shuffle projection leads to construction principles for pairs of languages closed under shuffle projection. Additionally, it is shown that under certain conditions these transductions are rational, which implies decidability of closure against shuffle projection. Decidability of these conditions is proven for regular languages. Finally, without additional conditions, decidability of the question, whether a pair of regular languages is closed under shuffle projection, is shown. In an appendix the relation between shuffle projection and the shuffle product of two languages is discussed. Additionally, a kind of shuffle product for computations in S-automata is defined. |
BibTeX:
@techreport{ochsenschlaeger:rieke:2015,
author = {Peter Ochsenschl\"ager and Roland Rieke},
title = {{Pairs of Languages Closed under Shuffle Projection}},
url="http://arxiv.org/abs/1503.08602",
publisher={arXiv},
year = {2015}
}
|
| Peter Ochsenschläger and Roland Rieke (2014), Safety by Construction: Well-behaved Scalable Systems, International Journal On Advances in Systems and Measurements, vol 7, no 3&4, 2014 [Abstract] [BibTeX] [Journal (free access)] [Author's version] |
| Abstract: This paper presents a formal framework that provides construction principles for well-behaved scalable systems, such that starting with a prototype system satisfying a desired safety property result in a scalable system satisfying a corresponding safety property, called scalable safety property. With respect to different aspects of scalability, the focus of this work is on property preserving structural scalability. At that, we consider systems composed of a varying set of individual components where individual components of the same type behave in the same manner, which is characteristic for the type. The respective properties can rely on specific component types and a specific number of individual components but not on the specific individuality of the components. Well-behaved scalable systems are characterised by those systems which fulfil such a kind of property if already one prototype system (depending on the property) fulfils that property. Sufficient conditions to specify a certain kind of basic well-behaved scalable systems are given and it is shown, how to construct more complex systems by the composition of several synchronisation conditions. Scalable safety properties can be used to express privacy policies as well as security and dependability requirements. It is demonstrated, how the parameterised problem of verifying such a property is reduced to a finite state problem for well-behaved scalable systems. The formal framework for well-behaved scalable systems is developed in terms of prefix closed formal languages and alphabetic language homomorphisms. |
BibTeX:
@article{SysMea14,
author={Peter Ochsenschl\"ager and Roland Rieke},
title={Safety by Construction: Well-behaved Scalable Systems},
year={2014},
journal = "International Journal On Advances in Systems and Measurements",
volume = "7",
number = "3 \& 4",
pages = "239 - 257",
issn = "1942-261x",
publisher = {IARIA}
}
|
| Peter Ochsenschläger and Roland Rieke (2014), Construction Principles for Well-behaved Scalable Systems, The Ninth International Conference on Systems (ICONS 2014) [Abstract] [BibTeX] [Paper (free access)] [Author's version] [Proofs] |
| Abstract: We formally define scalable systems as uniformly monotonic parameterised systems and motivate this definition. With respect to such scalable systems, we focus on properties, which rely on specific component types and a specific number of individual components for these component types but not on the specific individuality of the individual components. We characterise well-behaved scalable systems by those systems which fulfil such a kind of property if already one prototype system (depending on the property) fulfils that property. Self-similar uniformly monotonic parameterised systems have the above desired property. Therefore, we define well-behaved scalable systems as self-similar scalable systems. This paper presents a formal framework that provides construction principles for well-behaved scalable systems. It gives sufficient conditions to specify a certain kind of basic well-behaved scalable systems and shows how to construct more complex systems by the composition of several synchronisation conditions. |
BibTeX:
@incollection{ochsenschlaeger:rieke:2014,
author = {Peter Ochsenschl\"ager and Roland Rieke},
title = {{Construction Principles for Well-behaved Scalable Systems}},
booktitle = {ICONS 2014, The Ninth International Conference on Systems, February 23 - 27, 2014 - Nice, France},
url="http://www.thinkmind.org/download.php?articleid=icons_2014_2_30_40160",
pages="32-39",
issn="2308-4243",
isbn="978-1-61208-319-3",
publisher={IARIA},
year = {2014}
}
|
| Peter Ochsenschläger and Roland Rieke (2012), Reliability Aspects of Uniformly Parameterised Cooperations, The Seventh International Conference on Systems (ICONS 2012) [Abstract] [BibTeX] [Paper (free access)] [Author's version] |
| Abstract: In this paper, we examine reliability aspects of systems, which are characterised by the composition of a set of identical components. These components interact in a uniform manner, described by the schedules of the partners. Such kind of interaction is typical for scalable complex systems with cloud or grid structure. We call these systems ``uniformly parameterised cooperations''. We consider reliability of such systems in a possibilistic sense. This is formalised by always-eventually properties, a special class of liveness properties using a modified satisfaction relation, which expresses possibilities. As a main result, a finite state verification framework for uniformly parameterised reliability properties is given. The keys to this framework are structuring cooperations into phases and defining closed behaviours of systems. In order to verify reliability properties of such uniformly parameterised cooperations, we use finite state semi-algorithms that are independent of the concrete parameter setting. |
BibTeX:
@incollection{ochsenschlaeger:rieke:2012b,
author = {Peter Ochsenschläger and Roland Rieke},
title = {{Reliability Aspects of Uniformly Parameterised Cooperations}},
booktitle = {ICONS 2012, The Seventh International Conference on Systems, February 29 - March 5, 2012 - Saint Gilles, Reunion Island},
pages = {25-34},
url = {http://www.thinkmind.org/download.php?articleid=icons_2012_2_10_20024},
publisher={IARIA},
isbn={978-1-61208-184-7},
year = {2012}
}
|
| Peter Ochsenschläger and Roland Rieke (2012), Security Requirements for Uniformly Parameterised Cooperations, The 20th Euromicro International Conference on Parallel, Distributed and Network-Based Computing (PDP 2012) |
| Abstract: The specification of security requirements is an important step when specifying new systems and systems of systems or analysing existing systems with regard to security issues. A common way to formally specify security requirements is by means of safety and liveness properties. The systems in the focus of this paper are uniformly parameterised cooperations. Such systems are characterised by the composition of a set of identical components. These components interact in a uniform manner described by the schedules of the partners. Such a kind of interaction is typical for scalable complex systems with a cloud or grid structure. As a main result, a formalism to specify uniformly parameterised behaviour properties of cooperations is given. To capture possibilistic aspects of especially liveness properties, a modified satisfaction relation is used. For safety properties, this relation, which is called approximate satisfaction, is equivalent to the usual one. |
BibTeX:
@inproceedings{ochsenschlaeger:rieke:2012a,
author = {Peter Ochsenschläger and Roland Rieke},
title = {Security Requirements for Uniformly Parameterised Cooperations},
booktitle = {Parallel, Distributed and Network-Based Processing (PDP), 2012 20th Euromicro International Conference on},
volume = {0},
issn = {1066-6192},
year = {2012},
pages = {288-292},
url = {http://doi.ieeecomputersociety.org/10.1109/PDP.2012.27},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
|
| Peter Ochsenschläger and Roland Rieke (2011), Security Properties of Self-similar Uniformly Parameterised Systems of Cooperations, The 19th Euromicro Conference on Parallel, Distributed and Network-Based Computing (PDP 2011) |
| Abstract: Uniform parameterisations of cooperations are defined in terms of formal language theory, such that each pair of partners cooperates in the same manner, and that the mechanism (schedule) to determine how one partner may be involved in several cooperations, is the same for each partner. Generalising each pair of partners cooperating in the same manner, for such systems of cooperations a kind of self-similarity is formalised. From an abstracting point of view, where only actions of some selected partners are considered, the complex system of all partners behaves like the smaller subsystem of the selected partners. For verification purposes, so called uniformly parameterised safety properties are defined. Such properties can be used to express privacy policies as well as security and dependability requirements. It is shown, how the parameterised problem of verifying such a property is reduced by self-similarity to a finite state problem. |
BibTeX:
@inproceedings{ochsenschlaeger:rieke:2011,
author = {Peter Ochsenschläger and Roland Rieke},
title = {{Security Properties of Self-similar Uniformly Parameterised Systems of Cooperations}},
booktitle = {Proceedings of the 19th Euromicro Conference on Parallel, Distributed and Network-Based Processing},
pages = {640-645},
doi = {http://doi.ieeecomputersociety.org/10.1109/PDP.2011.57},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
year = {2011}
}
|
| Peter Ochsenschläger and Roland Rieke (2010), Behaviour Properties of Uniformly Parameterised Cooperations Fraunhofer SIT, Technical Report SIT-TR-2010/2, 2010. |
| Abstract: In this paper we consider safety and liveness properties, where possibilistic aspects of especially liveness properties are captured by a modified satisfaction relation, called approximate satisfaction. The systems in the focus of this paper are uniformly parameterised cooperations. Such systems are characterised by the composition of a set of identical components. These components interact in a uniform manner described by the schedules of the partners. Such kind of interaction is typical for scalable complex systems with cloud or grid structure. As a main result, a finite state verification framework for uniformly parameterised behaviour properties is given. The keys to this framework are structuring cooperations into phases and defining periods of system behaviour. Finite state semi-algorithms that are independent of the concrete parameter setting are presented to verify behaviour properties of such uniformly parameterised cooperations. |
BibTeX:
@techreport{OR2010t2,
author = {Peter Ochsenschl\"ager and Roland Rieke},
title = {Behaviour Properties of Uniformly Parameterised Cooperations},
year = {2010},
number = {SIT-TR-2010/2},
url = {http://publica.fraunhofer.de/dokumente/N-212198.html}
}
|
| Peter Ochsenschläger and Roland Rieke (2010), Uniform Parameterisation of Phase Based Cooperations. Fraunhofer SIT, Technical Report SIT-TR-2010/1, 2010. |
| Abstract: Uniform parameterisations of phase based cooperations are defined in terms of formal language theory. For such systems of cooperations a kind of self-similarity is formalised. Based on deterministic computations in shuffle automata a sufficient condition for self-similarity is given. Under certain regularity restrictions this condition can be verified by a semi-algorithm. For verification purposes, so called uniformly parameterised safety properties are defined, which e.g. can be used to express privacy policies. It is shown, how the parameterised problem of verifying such a property is reduced by self-similarity to a finite state problem. |
BibTeX:
@techreport{OR2010t,
author = {Peter Ochsenschl\"ager and Roland Rieke},
title = {Uniform Parameterisation of Phase Based Cooperations},
year = {2010},
number = {SIT-TR-2010/1},
url = {http://publica.fraunhofer.de/dokumente/N-212197.html}
}
|
| Peter Ochsenschläger and Roland Rieke (2007), Abstraction Based Verification of a Parameterised Policy Controlled System, MMM-ACNS-07, (Springer CCIS 1) |
| Abstract: Safety critical and business critical systems are usually controlled by policies with the objective to guarantee a variety of safety, liveness and security properties. Traditional model checking techniques allow a verification of the required behaviour only for systems with very few components. To be able to verify entire families of systems, independent of the exact number of replicated components, we developed an abstraction based approach to extend our current tool supported verification techniques to such families of systems that are usually parameterised by a number of replicated identical components. We demonstrate our technique by an exemplary verification of security and liveness properties of a simple parameterised collaboration scenario. Verification results for configurations with fixed numbers of components are used to choose an appropriate property preserving abstraction that provides the basis for an inductive proof that generalises the results for a family of systems with arbitrary settings of parameters. |
BibTeX:
@incollection{OR07,
author={Ochsenschl\"ager, Peter and Rieke, Roland},
title={Abstraction Based Verification of a Parameterised Policy Controlled System},
year={2007},
isbn={978-3-540-73985-2},
booktitle={Computer Network Security, Fourth International Conference on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2007 St. Petersburg, Russia, September 13-15, 2007 Proceedings},
volume={1},
series={Communications in Computer and Information Science},
editor={Gorodetsky, Vladimir and Kotenko, Igor and Skormin, VictorA.},
doi={10.1007/978-3-540-73986-9_19},
url={http://dx.doi.org/10.1007/978-3-540-73986-9_19},
publisher={Springer Berlin Heidelberg},
keywords={Formal analysis of security and liveness properties; security modelling and simulation; security policies; parameterised models},
pages={228-241},
language={English}
}
|
| Peter Ochsenschläger, Jürgen Repp, and Roland Rieke (2000), Verification of Cooperating Systems - An Approach Based on Formal Languages, In Proc. 13th International Florida Artificial Intelligence Research Society Conference (FLAIRS-2000), AAAI Press. |
BibTeX:
@inproceedings{Ochsenschlaeger:Repp:Rieke:2000a,
author = {Peter Ochsenschläger and Jürgen Repp and Rieke, R.},
title = {Verification of Cooperating Systems -- An Approach Based on Formal Languages},
booktitle = {Proc. 13th International Florida Artificial Intelligence Research Society Conference (FLAIRS-2000)},
publisher = {AAAI Press},
location={Orlando, FL, USA},
year = {2000},
month= {May},
pages = {346-350},
note = {Copyright: 2000, American Association for Artificial Intelligence (www.aaai.org). All rights reserved.},
url = {http://www.aaai.org/Papers/FLAIRS/2000/FLAIRS00-065.pdf}
}
|
| Peter Ochsenschläger, Jürgen Repp, and Roland Rieke (2000), Abstraction and composition - a verification method for co-operating systems, Journal of Experimental and Theoretical Artificial Intelligence, Volume 12, Issue 4, 2000. Taylor and Francis. |
BibTeX:
@article{Ochsenschlaeger:Repp:Rieke:2000c,
author = {Peter Ochsenschl\"ager and J\"urgen Repp and Roland Rieke},
title = {Abstraction and composition -- a verification method for co-operating systems},
journal = {Journal of Experimental and Theoretical Artificial Intelligence},
year = {2000},
month={October},
volume = {12},
number={4},
pages = {447-459},
issn= {0952-813X},
doi ={10.1080/095281300454829},
url={http://dx.doi.org/10.1080/095281300454829},
publisher = {Taylor and Francis Ltd},
}
|