About
SLEEC-TK is a publicly available toolkit, usable by non-technical experts, and it enables specification and verification of non-functional rules with the focus on SLEEC (social, legal, ethical, empathetic, and cultural) principles for autonomous agents. SLEEC-TK is an Eclipse-based environment for defining SLEEC rules in a domain-specific language with a timed process algebraic semantics. SLEEC-TK uses model checking to identify redundant nd conflicting rules, and to verify conformance of design models with SLEEC rules.
SLEEC-TK Language Syntax
SLEEC syntax is composed of defBlock and ruleBock. Definitions are recursively defined in the SLEEC language through events, measures or constants. Every event and measure have an eventID and measureID respectively. The ruleBlock consist of triggers, responses, and defeaters. A trigger can combine events as well as measures and expressions of them with any logical operation. Responses can be timed, and one can define deadlines and timeouts with responses through within construct. SLEEC-TK currently handles seconds, hours and days as time units in the language . In order to handle the situations where the response event cannot happen within a required time unit, we include the otherwise construct to order the events. The concept of defeaters are conducted with unless together with a condition.
SLEEC-TK Language Semantics into CSP
The tock-CSP processes that define the semantics of the rules are computed through a visitor pattern applied to each element of the SLEEC grammar syntax tree, with each SLEEC rule converted to a tock-CSP process. The computation is based on translation rules. Each event and measure is modelled in tock-CSP as a channel with measure types directly converted into existing CSP datatypes, or introduced as a new scalar datatype in CSP.