Abstrakt. Cellinjektion är en metod som används för leverans av små provämnen till en biologisk cell och används i stor utsträckning vid läkemedelsutveckling, geninjektion, intracytoplasmisk spermainjektion (ICSI) och in-virto fertilisering (IVF). Robotiska cellinsprutningssystem ger automatisering av processen i motsats till manuella och halvautomatiska cellinsprutningssystem, som kräver expertoperatörer och innebär tidskrävande processer och även har lägre framgångshastigheter. Automatiseringen av cellinjektionsprocessen uppnås genom kontroll av injektionskraften och planering av injektionspipettens rörelse. Traditionellt analyseras dessa system med hjälp av pappers- och pencil-proof och datorsimuleringsmetoder. Den förra är dock benägen för mänsklig terror och den senare baseras på de numeriska algoritmerna, där approximationen av de matematiska uttrycken introducerar felaktigheter i analysen. Formella metoder kan övervinna dessa begränsningar och därmed ge en korrekt analys av cellinsprutningssystemen. Modellkontroll, dvs. en statsbaserad formell metod, har nyligen föreslagits för analys av dessa system. Det innebär dock diskretisering av de differentialekvationer som används för att modellera systemets dynamik och därmed kompromisser om fullständigheten i analysen av dessa säkerhetskritiska system. I det här dokumentet föreslår vi att man ska använda sig av högre ordnings- och teorembevisning, en formalistisk metod som grundar sig på avdragsförmåga, för modellering och analys av robotcellinsprutningssystemens dynamiska beteende. Den föreslagna analysen, baserad på HOL Light theorem bevis, gjorde det möjligt för oss att identifiera vissa avvikelser i simulering och modellkontroll baserad analys av samma robot cell injektionssystem.
Nyligen tillhandahöll Rashid och Hasan REF den formella modelleringen och analysen av de 2-DOF robotiska cellinsprutningssystemen med hjälp av HOL Light.
Formal Analysis of Robotic Cell Injection Systems using Theorem Proving
{'venue': 'LNCS special issue on the theme of CyPhy 2017', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}